:: deftheorem Def20 defines subdivision SIMPLEX0:def 20 :
for X being set
for KX being SimplicialComplexStr of X
for P being Function
for b₄ being strict SimplicialComplexStr of X holds
( b₄ = subdivision (P,KX) iff ( [#] b₄ = [#] KX & ( for A being Subset of b₄ holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) ) );