:: deftheorem Def21 defines subdivision SIMPLEX0:def 21 :
for X being set
for KX being SimplicialComplexStr of X
for P being Function
for n being Nat
for b₅ being SimplicialComplexStr of X holds
( b₅ = subdivision (n,P,KX) iff ex F being Function st
( F . 0 = KX & F . n = b₅ & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) );