begin
theorem
Lm1:
for X being set ex F being subset-closed set st
( F = union { (bool x) where x is Element of X : x in X } & X c= F & ( for Y being set st X c= Y & Y is subset-closed holds
F c= Y ) )
:: deftheorem Def1 defines subset-closed_closure_of SIMPLEX0:def 1 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem
:: deftheorem Def2 defines the_subsets_with_limited_card SIMPLEX0:def 2 :
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem
begin
theorem Th14:
:: deftheorem Def3 defines vertex-like SIMPLEX0:def 3 :
:: deftheorem Def4 defines Vertices SIMPLEX0:def 4 :
:: deftheorem Def5 defines finite-vertices SIMPLEX0:def 5 :
:: deftheorem Def6 defines locally-finite SIMPLEX0:def 6 :
:: deftheorem Def7 defines empty-membered SIMPLEX0:def 7 :
:: deftheorem Def8 defines with_non-empty_elements SIMPLEX0:def 8 :
:: deftheorem Def9 defines SimplicialComplexStr SIMPLEX0:def 9 :
:: deftheorem Def10 defines total SIMPLEX0:def 10 :
Lm2:
for K being SimplicialComplexStr holds
( Vertices K is empty iff K is empty-membered )
Lm3:
for x being set
for K being SimplicialComplexStr
for S being Subset of K st S is simplex-like & x in S holds
x in Vertices K
Lm4:
for K being SimplicialComplexStr
for A being Subset of K st A is simplex-like holds
A c= Vertices K
Lm5:
for K being SimplicialComplexStr holds Vertices K = union the topology of K
Lm6:
for K being SimplicialComplexStr st K is finite-vertices holds
the topology of K is finite
theorem
theorem
theorem
theorem
theorem Th19:
theorem Th20:
begin
:: deftheorem defines Complex_of SIMPLEX0:def 11 :
theorem
begin
:: deftheorem Def12 defines degree SIMPLEX0:def 12 :
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
begin
:: deftheorem Def13 defines SubSimplicialComplex SIMPLEX0:def 13 :
theorem Th27:
theorem Th28:
theorem
theorem
theorem
theorem Th32:
:: deftheorem Def14 defines maximal SIMPLEX0:def 14 :
theorem Th33:
theorem Th34:
theorem
theorem Th36:
:: deftheorem Def15 defines | SIMPLEX0:def 15 :
:: deftheorem Def16 defines | SIMPLEX0:def 16 :
theorem Th37:
theorem
theorem
theorem
begin
:: deftheorem defines Skeleton_of SIMPLEX0:def 17 :
theorem
theorem
theorem
theorem
theorem
theorem
Lm7:
for i being Integer
for K being non void subset-closed SimplicialComplexStr st - 1 <= i & i <= degree K holds
ex S being Simplex of K st card S = i + 1
:: deftheorem Def18 defines Simplex SIMPLEX0:def 18 :
theorem
theorem
theorem
:: deftheorem Def19 defines Face SIMPLEX0:def 19 :
theorem
begin
:: deftheorem Def20 defines subdivision SIMPLEX0:def 20 :
theorem Th51:
theorem Th52:
theorem
theorem Th54:
theorem
theorem Th56:
theorem
theorem Th58:
theorem
theorem Th60:
:: deftheorem Def21 defines subdivision SIMPLEX0:def 21 :
theorem Th61:
theorem Th62:
theorem Th63:
theorem
theorem