:: Abstract Simplicial Complexes :: by Karol P\c{a}k :: :: Received December 18, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users begin notation let X be set ; antonym with_empty_element X for with_non-empty_elements ; end; registration cluster empty -> subset-closed for set ; coherence for b1 being set st b1 is empty holds b1 is subset-closed proofend; cluster with_empty_element -> non empty for set ; coherence for b1 being set st b1 is with_empty_element holds not b1 is empty by SETFAM_1:def_8; cluster non empty subset-closed -> with_empty_element for set ; coherence for b1 being set st not b1 is empty & b1 is subset-closed holds b1 is with_empty_element proofend; end; registration let X be set ; cluster Sub_of_Fin X -> finite-membered ; coherence Sub_of_Fin X is finite-membered proofend; end; registration let X be subset-closed set ; cluster Sub_of_Fin X -> subset-closed ; coherence Sub_of_Fin X is subset-closed proofend; end; theorem :: SIMPLEX0:1 for Y being set holds ( Y is subset-closed iff for X being set st X in Y holds bool X c= Y ) proofend; registration let A, B be subset-closed set ; clusterA \/ B -> subset-closed ; coherence A \/ B is subset-closed proofend; clusterA /\ B -> subset-closed ; coherence A /\ B is subset-closed proofend; end; 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 ) ) proofend; definition let X be set ; func subset-closed_closure_of X -> subset-closed set means :Def1: :: SIMPLEX0:def 1 ( X c= it & ( for Y being set st X c= Y & Y is subset-closed holds it c= Y ) ); existence ex b1 being subset-closed set st ( X c= b1 & ( for Y being set st X c= Y & Y is subset-closed holds b1 c= Y ) ) proofend; uniqueness for b1, b2 being subset-closed set st X c= b1 & ( for Y being set st X c= Y & Y is subset-closed holds b1 c= Y ) & X c= b2 & ( for Y being set st X c= Y & Y is subset-closed holds b2 c= Y ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines subset-closed_closure_of SIMPLEX0:def_1_:_ for X being set for b2 being subset-closed set holds ( b2 = subset-closed_closure_of X iff ( X c= b2 & ( for Y being set st X c= Y & Y is subset-closed holds b2 c= Y ) ) ); theorem Th2: :: SIMPLEX0:2 for x, X being set holds ( x in subset-closed_closure_of X iff ex y being set st ( x c= y & y in X ) ) proofend; definition let X be set ; let F be Subset-Family of X; :: original:subset-closed_closure_of redefine func subset-closed_closure_of F -> subset-closed Subset-Family of X; coherence subset-closed_closure_of F is subset-closed Subset-Family of X proofend; end; registration cluster subset-closed_closure_of {} -> empty subset-closed ; coherence subset-closed_closure_of {} is empty proofend; let X be non empty set ; cluster subset-closed_closure_of X -> non empty subset-closed ; coherence not subset-closed_closure_of X is empty proofend; end; registration let X be with_non-empty_element set ; cluster subset-closed_closure_of X -> with_non-empty_element subset-closed ; coherence not subset-closed_closure_of X is empty-membered proofend; end; registration let X be finite-membered set ; cluster subset-closed_closure_of X -> finite-membered subset-closed ; coherence subset-closed_closure_of X is finite-membered proofend; end; theorem Th3: :: SIMPLEX0:3 for X, Y being set st X c= Y & Y is subset-closed holds subset-closed_closure_of X c= Y proofend; theorem Th4: :: SIMPLEX0:4 for X being set holds subset-closed_closure_of {X} = bool X proofend; theorem :: SIMPLEX0:5 for X, Y being set holds subset-closed_closure_of (X \/ Y) = (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) proofend; theorem Th6: :: SIMPLEX0:6 for X, Y being set holds ( X is_finer_than Y iff subset-closed_closure_of X c= subset-closed_closure_of Y ) proofend; theorem Th7: :: SIMPLEX0:7 for X being set st X is subset-closed holds subset-closed_closure_of X = X proofend; theorem :: SIMPLEX0:8 for X being set st subset-closed_closure_of X c= X holds X is subset-closed proofend; definition let Y, X, n be set ; func the_subsets_with_limited_card (n,X,Y) -> Subset-Family of Y means :Def2: :: SIMPLEX0:def 2 for A being Subset of Y holds ( A in it iff ( A in X & card A c= card n ) ); existence ex b1 being Subset-Family of Y st for A being Subset of Y holds ( A in b1 iff ( A in X & card A c= card n ) ) proofend; uniqueness for b1, b2 being Subset-Family of Y st ( for A being Subset of Y holds ( A in b1 iff ( A in X & card A c= card n ) ) ) & ( for A being Subset of Y holds ( A in b2 iff ( A in X & card A c= card n ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines the_subsets_with_limited_card SIMPLEX0:def_2_:_ for Y, X, n being set for b4 being Subset-Family of Y holds ( b4 = the_subsets_with_limited_card (n,X,Y) iff for A being Subset of Y holds ( A in b4 iff ( A in X & card A c= card n ) ) ); registration let D be non empty set ; cluster with_non-empty_element finite finite-membered subset-closed for Element of bool (bool D); existence ex b1 being Subset-Family of D st ( b1 is finite & b1 is with_non-empty_element & b1 is subset-closed & b1 is finite-membered ) proofend; end; registration let Y, X be set ; let n be finite set ; cluster the_subsets_with_limited_card (n,X,Y) -> finite-membered ; coherence the_subsets_with_limited_card (n,X,Y) is finite-membered proofend; end; registration let Y be set ; let X be subset-closed set ; let n be set ; cluster the_subsets_with_limited_card (n,X,Y) -> subset-closed ; coherence the_subsets_with_limited_card (n,X,Y) is subset-closed proofend; end; registration let Y be set ; let X be with_empty_element set ; let n be set ; cluster the_subsets_with_limited_card (n,X,Y) -> with_empty_element ; coherence the_subsets_with_limited_card (n,X,Y) is with_empty_element proofend; end; registration let D be non empty set ; let X be with_non-empty_element subset-closed Subset-Family of D; let n be non empty set ; cluster the_subsets_with_limited_card (n,X,D) -> with_non-empty_element ; coherence not the_subsets_with_limited_card (n,X,D) is empty-membered proofend; end; notation let X be set ; let Y be Subset-Family of X; let n be set ; synonym the_subsets_with_limited_card (n,Y) for the_subsets_with_limited_card (n,Y,X); end; theorem Th9: :: SIMPLEX0:9 for X being set st not X is empty & X is finite & X is c=-linear holds union X in X proofend; theorem Th10: :: SIMPLEX0:10 for X being c=-linear finite set st X is with_non-empty_elements holds card X c= card (union X) proofend; theorem :: SIMPLEX0:11 for X, x being set st X is c=-linear holds X \/ {((union X) \/ x)} is c=-linear proofend; theorem Th12: :: SIMPLEX0:12 for X being non empty set ex Y being Subset-Family of X st ( Y is with_non-empty_elements & Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds ex x being set st ( x in Z & Z \ {x} in Y ) ) ) proofend; theorem :: SIMPLEX0:13 for X being set for Y being Subset-Family of X st Y is finite & Y is with_non-empty_elements & Y is c=-linear & X in Y holds ex Y1 being Subset-Family of X st ( Y c= Y1 & Y1 is with_non-empty_elements & Y1 is c=-linear & card X = card Y1 & ( for Z being set st Z in Y1 & card Z <> 1 holds ex x being set st ( x in Z & Z \ {x} in Y1 ) ) ) proofend; begin definition mode SimplicialComplexStr is TopStruct ; end; notation let K be SimplicialComplexStr; let A be Subset of K; synonym simplex-like A for open ; end; notation let K be SimplicialComplexStr; let S be Subset-Family of K; synonym simplex-like S for open ; end; registration let K be SimplicialComplexStr; cluster empty simplex-like for Element of bool (bool the carrier of K); existence ex b1 being Subset-Family of K st ( b1 is empty & b1 is simplex-like ) proofend; end; theorem Th14: :: SIMPLEX0:14 for K being SimplicialComplexStr for S being Subset-Family of K holds ( S is simplex-like iff S c= the topology of K ) proofend; definition let K be SimplicialComplexStr; let v be Element of K; attrv is vertex-like means :Def3: :: SIMPLEX0:def 3 ex S being Subset of K st ( S is simplex-like & v in S ); end; :: deftheorem Def3 defines vertex-like SIMPLEX0:def_3_:_ for K being SimplicialComplexStr for v being Element of K holds ( v is vertex-like iff ex S being Subset of K st ( S is simplex-like & v in S ) ); definition let K be SimplicialComplexStr; func Vertices K -> Subset of K means :Def4: :: SIMPLEX0:def 4 for v being Element of K holds ( v in it iff v is vertex-like ); existence ex b1 being Subset of K st for v being Element of K holds ( v in b1 iff v is vertex-like ) proofend; uniqueness for b1, b2 being Subset of K st ( for v being Element of K holds ( v in b1 iff v is vertex-like ) ) & ( for v being Element of K holds ( v in b2 iff v is vertex-like ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines Vertices SIMPLEX0:def_4_:_ for K being SimplicialComplexStr for b2 being Subset of K holds ( b2 = Vertices K iff for v being Element of K holds ( v in b2 iff v is vertex-like ) ); definition let K be SimplicialComplexStr; mode Vertex of K is Element of Vertices K; end; definition let K be SimplicialComplexStr; attrK is finite-vertices means :Def5: :: SIMPLEX0:def 5 Vertices K is finite ; end; :: deftheorem Def5 defines finite-vertices SIMPLEX0:def_5_:_ for K being SimplicialComplexStr holds ( K is finite-vertices iff Vertices K is finite ); definition let K be SimplicialComplexStr; attrK is locally-finite means :Def6: :: SIMPLEX0:def 6 for v being Vertex of K holds { S where S is Subset of K : ( S is simplex-like & v in S ) } is finite ; end; :: deftheorem Def6 defines locally-finite SIMPLEX0:def_6_:_ for K being SimplicialComplexStr holds ( K is locally-finite iff for v being Vertex of K holds { S where S is Subset of K : ( S is simplex-like & v in S ) } is finite ); definition let K be SimplicialComplexStr; attrK is empty-membered means :Def7: :: SIMPLEX0:def 7 the topology of K is empty-membered ; attrK is with_non-empty_elements means :Def8: :: SIMPLEX0:def 8 the topology of K is with_non-empty_elements ; end; :: deftheorem Def7 defines empty-membered SIMPLEX0:def_7_:_ for K being SimplicialComplexStr holds ( K is empty-membered iff the topology of K is empty-membered ); :: deftheorem Def8 defines with_non-empty_elements SIMPLEX0:def_8_:_ for K being SimplicialComplexStr holds ( K is with_non-empty_elements iff the topology of K is with_non-empty_elements ); notation let K be SimplicialComplexStr; antonym with_non-empty_element K for empty-membered ; antonym with_empty_element K for with_non-empty_elements ; end; definition let X be set ; mode SimplicialComplexStr of X -> SimplicialComplexStr means :Def9: :: SIMPLEX0:def 9 [#] it c= X; existence ex b1 being SimplicialComplexStr st [#] b1 c= X proofend; end; :: deftheorem Def9 defines SimplicialComplexStr SIMPLEX0:def_9_:_ for X being set for b2 being SimplicialComplexStr holds ( b2 is SimplicialComplexStr of X iff [#] b2 c= X ); definition let X be set ; let KX be SimplicialComplexStr of X; attrKX is total means :Def10: :: SIMPLEX0:def 10 [#] KX = X; end; :: deftheorem Def10 defines total SIMPLEX0:def_10_:_ for X being set for KX being SimplicialComplexStr of X holds ( KX is total iff [#] KX = X ); Lm2: for K being SimplicialComplexStr holds ( Vertices K is empty iff K is empty-membered ) proofend; 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 proofend; Lm4: for K being SimplicialComplexStr for A being Subset of K st A is simplex-like holds A c= Vertices K proofend; Lm5: for K being SimplicialComplexStr holds Vertices K = union the topology of K proofend; Lm6: for K being SimplicialComplexStr st K is finite-vertices holds the topology of K is finite proofend; registration cluster with_empty_element -> non void for TopStruct ; coherence for b1 being SimplicialComplexStr st b1 is with_empty_element holds not b1 is void proofend; cluster with_non-empty_element -> non void for TopStruct ; coherence for b1 being SimplicialComplexStr st b1 is with_non-empty_element holds not b1 is void proofend; cluster non void empty-membered -> with_empty_element for TopStruct ; coherence for b1 being SimplicialComplexStr st not b1 is void & b1 is empty-membered holds b1 is with_empty_element proofend; cluster non void subset-closed -> with_empty_element for TopStruct ; coherence for b1 being SimplicialComplexStr st not b1 is void & b1 is subset-closed holds b1 is with_empty_element proofend; cluster empty-membered -> subset-closed finite-vertices for TopStruct ; coherence for b1 being SimplicialComplexStr st b1 is empty-membered holds ( b1 is subset-closed & b1 is finite-vertices ) proofend; cluster finite-vertices -> finite-degree locally-finite for TopStruct ; coherence for b1 being SimplicialComplexStr st b1 is finite-vertices holds ( b1 is locally-finite & b1 is finite-degree ) proofend; cluster subset-closed locally-finite -> finite-membered for TopStruct ; coherence for b1 being SimplicialComplexStr st b1 is locally-finite & b1 is subset-closed holds b1 is finite-membered proofend; end; registration let X be set ; cluster empty strict void empty-membered for SimplicialComplexStr of X; existence ex b1 being SimplicialComplexStr of X st ( b1 is empty & b1 is void & b1 is empty-membered & b1 is strict ) proofend; end; registration let D be non empty set ; cluster non empty strict non void empty-membered total for SimplicialComplexStr of D; existence ex b1 being SimplicialComplexStr of D st ( not b1 is empty & not b1 is void & b1 is total & b1 is empty-membered & b1 is strict ) proofend; cluster non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element total for SimplicialComplexStr of D; existence ex b1 being SimplicialComplexStr of D st ( not b1 is empty & b1 is total & b1 is with_empty_element & b1 is with_non-empty_element & b1 is finite-vertices & b1 is subset-closed & b1 is strict ) proofend; end; registration cluster non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element for TopStruct ; existence ex b1 being SimplicialComplexStr st ( not b1 is empty & b1 is with_empty_element & b1 is with_non-empty_element & b1 is finite-vertices & b1 is subset-closed & b1 is strict ) proofend; end; registration let K be with_non-empty_element SimplicialComplexStr; cluster Vertices K -> non empty ; coherence not Vertices K is empty by Lm2; end; registration let K be finite-vertices SimplicialComplexStr; cluster simplex-like -> finite for Element of bool (bool the carrier of K); coherence for b1 being Subset-Family of K st b1 is simplex-like holds b1 is finite proofend; end; registration let K be finite-membered SimplicialComplexStr; cluster simplex-like -> finite-membered for Element of bool (bool the carrier of K); coherence for b1 being Subset-Family of K st b1 is simplex-like holds b1 is finite-membered proofend; end; theorem :: SIMPLEX0:15 for K being SimplicialComplexStr holds ( Vertices K is empty iff K is empty-membered ) by Lm2; theorem :: SIMPLEX0:16 for K being SimplicialComplexStr holds Vertices K = union the topology of K by Lm5; theorem :: SIMPLEX0:17 for K being SimplicialComplexStr for S being Subset of K st S is simplex-like holds S c= Vertices K by Lm4; theorem :: SIMPLEX0:18 for K being SimplicialComplexStr st K is finite-vertices holds the topology of K is finite by Lm6; theorem Th19: :: SIMPLEX0:19 for K being SimplicialComplexStr st the topology of K is finite & not K is finite-vertices holds not K is finite-membered proofend; theorem Th20: :: SIMPLEX0:20 for K being SimplicialComplexStr st K is subset-closed & the topology of K is finite holds K is finite-vertices proofend; begin definition let X be set ; let Y be Subset-Family of X; func Complex_of Y -> strict SimplicialComplexStr of X equals :: SIMPLEX0:def 11 TopStruct(# X,(subset-closed_closure_of Y) #); coherence TopStruct(# X,(subset-closed_closure_of Y) #) is strict SimplicialComplexStr of X proofend; end; :: deftheorem defines Complex_of SIMPLEX0:def_11_:_ for X being set for Y being Subset-Family of X holds Complex_of Y = TopStruct(# X,(subset-closed_closure_of Y) #); registration let X be set ; let Y be Subset-Family of X; cluster Complex_of Y -> strict subset-closed total ; coherence ( Complex_of Y is total & Complex_of Y is subset-closed ) proofend; end; registration let X be set ; let Y be non empty Subset-Family of X; cluster Complex_of Y -> strict with_empty_element ; coherence not Complex_of Y is with_non-empty_elements by Def8; end; registration let X be set ; let Y be finite-membered Subset-Family of X; cluster Complex_of Y -> strict finite-membered ; coherence Complex_of Y is finite-membered proofend; end; registration let X be set ; let Y be finite finite-membered Subset-Family of X; cluster Complex_of Y -> strict finite-vertices ; coherence Complex_of Y is finite-vertices proofend; end; theorem :: SIMPLEX0:21 for K being SimplicialComplexStr st K is subset-closed holds TopStruct(# the carrier of K, the topology of K #) = Complex_of the topology of K proofend; definition let X be set ; mode SimplicialComplex of X is subset-closed finite-membered SimplicialComplexStr of X; end; definition let K be non void SimplicialComplexStr; mode Simplex of K is simplex-like Subset of K; end; registration let K be with_empty_element SimplicialComplexStr; cluster empty -> simplex-like for Element of bool the carrier of K; coherence for b1 being Subset of K st b1 is empty holds b1 is simplex-like proofend; cluster empty simplex-like for Element of bool the carrier of K; existence ex b1 being Simplex of K st b1 is empty proofend; end; registration let K be non void finite-membered SimplicialComplexStr; cluster finite simplex-like for Element of bool the carrier of K; existence ex b1 being Simplex of K st b1 is finite proofend; end; begin definition let K be SimplicialComplexStr; func degree K -> ext-real number means :Def12: :: SIMPLEX0:def 12 ( ( for S being finite Subset of K st S is simplex-like holds card S <= it + 1 ) & ex S being Subset of K st ( S is simplex-like & card S = it + 1 ) ) if ( not K is void & K is finite-degree ) it = - 1 if K is void otherwise it = +infty ; existence ( ( not K is void & K is finite-degree implies ex b1 being ext-real number st ( ( for S being finite Subset of K st S is simplex-like holds card S <= b1 + 1 ) & ex S being Subset of K st ( S is simplex-like & card S = b1 + 1 ) ) ) & ( K is void implies ex b1 being ext-real number st b1 = - 1 ) & ( ( K is void or not K is finite-degree ) & not K is void implies ex b1 being ext-real number st b1 = +infty ) ) proofend; uniqueness for b1, b2 being ext-real number holds ( ( not K is void & K is finite-degree & ( for S being finite Subset of K st S is simplex-like holds card S <= b1 + 1 ) & ex S being Subset of K st ( S is simplex-like & card S = b1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds card S <= b2 + 1 ) & ex S being Subset of K st ( S is simplex-like & card S = b2 + 1 ) implies b1 = b2 ) & ( K is void & b1 = - 1 & b2 = - 1 implies b1 = b2 ) & ( ( K is void or not K is finite-degree ) & not K is void & b1 = +infty & b2 = +infty implies b1 = b2 ) ) proofend; consistency for b1 being ext-real number st not K is void & K is finite-degree & K is void holds ( ( ( for S being finite Subset of K st S is simplex-like holds card S <= b1 + 1 ) & ex S being Subset of K st ( S is simplex-like & card S = b1 + 1 ) ) iff b1 = - 1 ) ; end; :: deftheorem Def12 defines degree SIMPLEX0:def_12_:_ for K being SimplicialComplexStr for b2 being ext-real number holds ( ( not K is void & K is finite-degree implies ( b2 = degree K iff ( ( for S being finite Subset of K st S is simplex-like holds card S <= b2 + 1 ) & ex S being Subset of K st ( S is simplex-like & card S = b2 + 1 ) ) ) ) & ( K is void implies ( b2 = degree K iff b2 = - 1 ) ) & ( ( K is void or not K is finite-degree ) & not K is void implies ( b2 = degree K iff b2 = +infty ) ) ); registration let K be finite-degree SimplicialComplexStr; cluster(degree K) + 1 -> natural ; coherence (degree K) + 1 is natural proofend; cluster degree K -> ext-real integer ; coherence degree K is integer proofend; end; theorem Th22: :: SIMPLEX0:22 for K being SimplicialComplexStr holds ( degree K = - 1 iff K is empty-membered ) proofend; theorem Th23: :: SIMPLEX0:23 for K being SimplicialComplexStr holds - 1 <= degree K proofend; theorem Th24: :: SIMPLEX0:24 for K being SimplicialComplexStr for S being finite Subset of K st S is simplex-like holds card S <= (degree K) + 1 proofend; theorem Th25: :: SIMPLEX0:25 for i being Integer for K being SimplicialComplexStr st ( not K is void or i >= - 1 ) holds ( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds card S <= i + 1 ) ) ) proofend; theorem :: SIMPLEX0:26 for X being set for A being finite Subset of X holds degree (Complex_of {A}) = (card A) - 1 proofend; begin definition let X be set ; let KX be SimplicialComplexStr of X; mode SubSimplicialComplex of KX -> SimplicialComplex of X means :Def13: :: SIMPLEX0:def 13 ( [#] it c= [#] KX & the topology of it c= the topology of KX ); existence ex b1 being SimplicialComplex of X st ( [#] b1 c= [#] KX & the topology of b1 c= the topology of KX ) proofend; end; :: deftheorem Def13 defines SubSimplicialComplex SIMPLEX0:def_13_:_ for X being set for KX being SimplicialComplexStr of X for b3 being SimplicialComplex of X holds ( b3 is SubSimplicialComplex of KX iff ( [#] b3 c= [#] KX & the topology of b3 c= the topology of KX ) ); registration let X be set ; let KX be SimplicialComplexStr of X; cluster empty strict void subset-closed finite-membered for SubSimplicialComplex of KX; existence ex b1 being SubSimplicialComplex of KX st ( b1 is empty & b1 is void & b1 is strict ) proofend; end; registration let X be set ; let KX be void SimplicialComplexStr of X; cluster -> void for SubSimplicialComplex of KX; coherence for b1 being SubSimplicialComplex of KX holds b1 is void proofend; end; registration let D be non empty set ; let KD be non void subset-closed SimplicialComplexStr of D; cluster non void subset-closed finite-membered for SubSimplicialComplex of KD; existence not for b1 being SubSimplicialComplex of KD holds b1 is void proofend; end; registration let X be set ; let KX be finite-vertices SimplicialComplexStr of X; cluster -> finite-vertices for SubSimplicialComplex of KX; coherence for b1 being SubSimplicialComplex of KX holds b1 is finite-vertices proofend; end; registration let X be set ; let KX be finite-degree SimplicialComplexStr of X; cluster -> finite-degree for SubSimplicialComplex of KX; coherence for b1 being SubSimplicialComplex of KX holds b1 is finite-degree proofend; end; theorem Th27: :: SIMPLEX0:27 for X being set for KX being SimplicialComplexStr of X for SX being SubSimplicialComplex of KX for S1 being SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX proofend; theorem Th28: :: SIMPLEX0:28 for X being set for KX being SimplicialComplexStr of X for A being Subset of KX for S being finite-membered Subset-Family of A st subset-closed_closure_of S c= the topology of KX holds Complex_of S is strict SubSimplicialComplex of KX proofend; theorem :: SIMPLEX0:29 for X being set for KX being subset-closed SimplicialComplexStr of X for A being Subset of KX for S being finite-membered Subset-Family of A st S c= the topology of KX holds Complex_of S is strict SubSimplicialComplex of KX proofend; theorem :: SIMPLEX0:30 for X being set for Y1, Y2 being Subset-Family of X st Y1 is finite-membered & Y1 is_finer_than Y2 holds Complex_of Y1 is SubSimplicialComplex of Complex_of Y2 proofend; theorem :: SIMPLEX0:31 for X being set for KX being SimplicialComplexStr of X for SX being SubSimplicialComplex of KX holds Vertices SX c= Vertices KX proofend; theorem Th32: :: SIMPLEX0:32 for X being set for KX being SimplicialComplexStr of X for SX being SubSimplicialComplex of KX holds degree SX <= degree KX proofend; definition let X be set ; let KX be SimplicialComplexStr of X; let SX be SubSimplicialComplex of KX; attrSX is maximal means :Def14: :: SIMPLEX0:def 14 for A being Subset of SX st A in the topology of KX holds A is simplex-like ; end; :: deftheorem Def14 defines maximal SIMPLEX0:def_14_:_ for X being set for KX being SimplicialComplexStr of X for SX being SubSimplicialComplex of KX holds ( SX is maximal iff for A being Subset of SX st A in the topology of KX holds A is simplex-like ); theorem Th33: :: SIMPLEX0:33 for X being set for KX being SimplicialComplexStr of X for SX being SubSimplicialComplex of KX holds ( SX is maximal iff (bool ([#] SX)) /\ the topology of KX c= the topology of SX ) proofend; registration let X be set ; let KX be SimplicialComplexStr of X; cluster strict subset-closed finite-membered maximal for SubSimplicialComplex of KX; existence ex b1 being SubSimplicialComplex of KX st ( b1 is maximal & b1 is strict ) proofend; end; theorem Th34: :: SIMPLEX0:34 for X being set for KX being SimplicialComplexStr of X for SX being SubSimplicialComplex of KX for S1 being SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds S1 is maximal SubSimplicialComplex of KX proofend; theorem :: SIMPLEX0:35 for X being set for KX being SimplicialComplexStr of X for SX being SubSimplicialComplex of KX for S1 being SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds S1 is maximal proofend; theorem Th36: :: SIMPLEX0:36 for X being set for KX being SimplicialComplexStr of X for K1, K2 being maximal SubSimplicialComplex of KX st [#] K1 = [#] K2 holds TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) proofend; definition let X be set ; let KX be subset-closed SimplicialComplexStr of X; let A be Subset of KX; assume A1: (bool A) /\ the topology of KX is finite-membered ; funcKX | A -> strict maximal SubSimplicialComplex of KX means :Def15: :: SIMPLEX0:def 15 [#] it = A; existence ex b1 being strict maximal SubSimplicialComplex of KX st [#] b1 = A proofend; uniqueness for b1, b2 being strict maximal SubSimplicialComplex of KX st [#] b1 = A & [#] b2 = A holds b1 = b2 by Th36; end; :: deftheorem Def15 defines | SIMPLEX0:def_15_:_ for X being set for KX being subset-closed SimplicialComplexStr of X for A being Subset of KX st (bool A) /\ the topology of KX is finite-membered holds for b4 being strict maximal SubSimplicialComplex of KX holds ( b4 = KX | A iff [#] b4 = A ); definition let X be set ; let SC be SimplicialComplex of X; let A be Subset of SC; redefine func SC | A means :Def16: :: SIMPLEX0:def 16 [#] it = A; compatibility for b1 being strict maximal SubSimplicialComplex of SC holds ( b1 = SC | A iff [#] b1 = A ) proofend; end; :: deftheorem Def16 defines | SIMPLEX0:def_16_:_ for X being set for SC being SimplicialComplex of X for A being Subset of SC for b4 being strict maximal SubSimplicialComplex of SC holds ( b4 = SC | A iff [#] b4 = A ); theorem Th37: :: SIMPLEX0:37 for X being set for SC being SimplicialComplex of X for A being Subset of SC holds the topology of (SC | A) = (bool A) /\ the topology of SC proofend; theorem :: SIMPLEX0:38 for X being set for SC being SimplicialComplex of X for A, B being Subset of SC for B1 being Subset of (SC | A) st B1 = B holds (SC | A) | B1 = SC | B proofend; theorem :: SIMPLEX0:39 for X being set for SC being SimplicialComplex of X holds SC | ([#] SC) = TopStruct(# the carrier of SC, the topology of SC #) proofend; theorem :: SIMPLEX0:40 for X being set for SC being SimplicialComplex of X for A, B being Subset of SC st A c= B holds SC | A is SubSimplicialComplex of SC | B proofend; registration cluster integer -> finite for set ; coherence for b1 being Integer holds b1 is finite proofend; end; begin definition let X be set ; let KX be SimplicialComplexStr of X; let i be real number ; func Skeleton_of (KX,i) -> SimplicialComplexStr of X equals :: SIMPLEX0:def 17 Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX)); coherence Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX)) is SimplicialComplexStr of X proofend; end; :: deftheorem defines Skeleton_of SIMPLEX0:def_17_:_ for X being set for KX being SimplicialComplexStr of X for i being real number holds Skeleton_of (KX,i) = Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX)); registration let X be set ; let KX be SimplicialComplexStr of X; cluster Skeleton_of (KX,(- 1)) -> empty-membered ; coherence Skeleton_of (KX,(- 1)) is empty-membered proofend; let i be Integer; cluster Skeleton_of (KX,i) -> finite-degree ; coherence Skeleton_of (KX,i) is finite-degree proofend; end; registration let X be set ; let KX be empty-membered SimplicialComplexStr of X; let i be Integer; cluster Skeleton_of (KX,i) -> empty-membered ; coherence Skeleton_of (KX,i) is empty-membered proofend; end; registration let D be non empty set ; let KD be non void subset-closed SimplicialComplexStr of D; let i be Integer; cluster Skeleton_of (KD,i) -> non void ; coherence not Skeleton_of (KD,i) is void proofend; end; theorem :: SIMPLEX0:41 for X being set for i1, i2 being Integer for KX being SimplicialComplexStr of X st - 1 <= i1 & i1 <= i2 holds Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2) proofend; definition let X be set ; let KX be subset-closed SimplicialComplexStr of X; let i be Integer; :: original:Skeleton_of redefine func Skeleton_of (KX,i) -> SubSimplicialComplex of KX; coherence Skeleton_of (KX,i) is SubSimplicialComplex of KX proofend; end; theorem :: SIMPLEX0:42 for X being set for i being Integer for KX being SimplicialComplexStr of X st KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered holds i = - 1 proofend; theorem :: SIMPLEX0:43 for X being set for i being Integer for KX being SimplicialComplexStr of X holds degree (Skeleton_of (KX,i)) <= degree KX proofend; theorem :: SIMPLEX0:44 for X being set for i being Integer for KX being SimplicialComplexStr of X st - 1 <= i holds degree (Skeleton_of (KX,i)) <= i proofend; theorem :: SIMPLEX0:45 for X being set for i being Integer for KX being SimplicialComplexStr of X st - 1 <= i & Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) holds degree KX <= i proofend; theorem :: SIMPLEX0:46 for X being set for i being Integer for KX being SimplicialComplexStr of X st KX is subset-closed & degree KX <= i holds Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) proofend; 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 proofend; definition let K be non void subset-closed SimplicialComplexStr; let i be real number ; assume B1: i is integer ; mode Simplex of i,K -> finite Simplex of K means :Def18: :: SIMPLEX0:def 18 card it = i + 1 if ( - 1 <= i & i <= degree K ) otherwise it is empty ; existence ( ( - 1 <= i & i <= degree K implies ex b1 being finite Simplex of K st card b1 = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b1 being finite Simplex of K st b1 is empty ) ) proofend; correctness consistency for b1 being finite Simplex of K holds verum; ; end; :: deftheorem Def18 defines Simplex SIMPLEX0:def_18_:_ for K being non void subset-closed SimplicialComplexStr for i being real number st i is integer holds for b3 being finite Simplex of K holds ( ( - 1 <= i & i <= degree K implies ( b3 is Simplex of i,K iff card b3 = i + 1 ) ) & ( ( not - 1 <= i or not i <= degree K ) implies ( b3 is Simplex of i,K iff b3 is empty ) ) ); registration let K be non void subset-closed SimplicialComplexStr; cluster -> empty for Simplex of - 1,K; coherence for b1 being Simplex of - 1,K holds b1 is empty proofend; end; theorem :: SIMPLEX0:47 for i being Integer for K being non void subset-closed SimplicialComplexStr for S being Simplex of i,K st not S is empty holds i is natural proofend; theorem :: SIMPLEX0:48 for K being non void subset-closed SimplicialComplexStr for S being finite Simplex of K holds S is Simplex of (card S) - 1,K proofend; theorem :: SIMPLEX0:49 for D being non empty set for K being non void subset-closed SimplicialComplexStr of D for S being non void SubSimplicialComplex of K for i being Integer for A being Simplex of i,S st ( not A is empty or i <= degree S or degree S = degree K ) holds A is Simplex of i,K proofend; definition let K be non void subset-closed SimplicialComplexStr; let i be real number ; assume that B1: i is integer and B2: i <= degree K ; let S be Simplex of i,K; mode Face of S -> Simplex of max ((i - 1),(- 1)),K means :Def19: :: SIMPLEX0:def 19 it c= S; existence ex b1 being Simplex of max ((i - 1),(- 1)),K st b1 c= S proofend; end; :: deftheorem Def19 defines Face SIMPLEX0:def_19_:_ for K being non void subset-closed SimplicialComplexStr for i being real number st i is integer & i <= degree K holds for S being Simplex of i,K for b4 being Simplex of max ((i - 1),(- 1)),K holds ( b4 is Face of S iff b4 c= S ); theorem :: SIMPLEX0:50 for X being set for n being Nat for K being non void subset-closed SimplicialComplexStr for S being Simplex of n,K st n <= degree K holds ( X is Face of S iff ex x being set st ( x in S & S \ {x} = X ) ) proofend; begin definition let X be set ; let KX be SimplicialComplexStr of X; let P be Function; func subdivision (P,KX) -> strict SimplicialComplexStr of X means :Def20: :: SIMPLEX0:def 20 ( [#] it = [#] KX & ( for A being Subset of it holds ( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) ); existence ex b1 being strict SimplicialComplexStr of X st ( [#] b1 = [#] KX & ( for A being Subset of b1 holds ( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) ) proofend; uniqueness for b1, b2 being strict SimplicialComplexStr of X st [#] b1 = [#] KX & ( for A being Subset of b1 holds ( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) & [#] b2 = [#] KX & ( for A being Subset of b2 holds ( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) holds b1 = b2 proofend; end; :: deftheorem Def20 defines subdivision SIMPLEX0:def_20_:_ for X being set for KX being SimplicialComplexStr of X for P being Function for b4 being strict SimplicialComplexStr of X holds ( b4 = subdivision (P,KX) iff ( [#] b4 = [#] KX & ( for A being Subset of b4 holds ( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) ) ); registration let X be set ; let KX be SimplicialComplexStr of X; let P be Function; cluster subdivision (P,KX) -> strict subset-closed finite-membered with_empty_element ; coherence ( not subdivision (P,KX) is with_non-empty_elements & subdivision (P,KX) is subset-closed & subdivision (P,KX) is finite-membered ) proofend; end; registration let X be set ; let KX be void SimplicialComplexStr of X; let P be Function; cluster subdivision (P,KX) -> strict empty-membered ; coherence subdivision (P,KX) is empty-membered proofend; end; theorem Th51: :: SIMPLEX0:51 for X being set for KX being SimplicialComplexStr of X for P being Function holds degree (subdivision (P,KX)) <= (degree KX) + 1 proofend; theorem Th52: :: SIMPLEX0:52 for X being set for KX being SimplicialComplexStr of X for P being Function st dom P is with_non-empty_elements holds degree (subdivision (P,KX)) <= degree KX proofend; registration let X be set ; let KX be finite-degree SimplicialComplexStr of X; let P be Function; cluster subdivision (P,KX) -> strict finite-degree ; coherence subdivision (P,KX) is finite-degree proofend; end; registration let X be set ; let KX be finite-vertices SimplicialComplexStr of X; let P be Function; cluster subdivision (P,KX) -> strict finite-vertices ; coherence subdivision (P,KX) is finite-vertices proofend; end; theorem :: SIMPLEX0:53 for X being set for KX being subset-closed SimplicialComplexStr of X for P being Function st dom P is with_non-empty_elements & ( for n being Nat st n <= degree KX holds ex S being Subset of KX st ( S is simplex-like & card S = n + 1 & BOOL S c= dom P & P .: (BOOL S) is Subset of KX & P | (BOOL S) is one-to-one ) ) holds degree (subdivision (P,KX)) = degree KX proofend; theorem Th54: :: SIMPLEX0:54 for X, Y, Z being set for KX being SimplicialComplexStr of X for P being Function st Y c= Z holds subdivision ((P | Y),KX) is SubSimplicialComplex of subdivision ((P | Z),KX) proofend; theorem :: SIMPLEX0:55 for X, Y being set for KX being SimplicialComplexStr of X for P being Function st (dom P) /\ the topology of KX c= Y holds subdivision ((P | Y),KX) = subdivision (P,KX) proofend; theorem Th56: :: SIMPLEX0:56 for X, Y, Z being set for KX being SimplicialComplexStr of X for P being Function st Y c= Z holds subdivision ((Y |` P),KX) is SubSimplicialComplex of subdivision ((Z |` P),KX) proofend; theorem :: SIMPLEX0:57 for X, Y being set for KX being SimplicialComplexStr of X for P being Function st P .: the topology of KX c= Y holds subdivision ((Y |` P),KX) = subdivision (P,KX) proofend; theorem Th58: :: SIMPLEX0:58 for X being set for KX being SimplicialComplexStr of X for SX being SubSimplicialComplex of KX for P being Function holds subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX) proofend; theorem :: SIMPLEX0:59 for X being set for KX being SimplicialComplexStr of X for SX being SubSimplicialComplex of KX for P being Function for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds subdivision (P,SX) = (subdivision (P,KX)) | A proofend; theorem Th60: :: SIMPLEX0:60 for X being set for P being Function for K1, K2 being SimplicialComplexStr of X st TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) holds subdivision (P,K1) = subdivision (P,K2) proofend; definition let X be set ; let KX be SimplicialComplexStr of X; let P be Function; let n be Nat; func subdivision (n,P,KX) -> SimplicialComplexStr of X means :Def21: :: SIMPLEX0:def 21 ex F being Function st ( F . 0 = KX & F . n = it & dom F = NAT & ( for k being Nat for KX1 being SimplicialComplexStr of X st KX1 = F . k holds F . (k + 1) = subdivision (P,KX1) ) ); existence ex b1 being SimplicialComplexStr of X ex F being Function st ( F . 0 = KX & F . n = b1 & dom F = NAT & ( for k being Nat for KX1 being SimplicialComplexStr of X st KX1 = F . k holds F . (k + 1) = subdivision (P,KX1) ) ) proofend; uniqueness for b1, b2 being SimplicialComplexStr of X st ex F being Function st ( F . 0 = KX & F . n = b1 & dom F = NAT & ( for k being Nat for KX1 being SimplicialComplexStr of X st KX1 = F . k holds F . (k + 1) = subdivision (P,KX1) ) ) & ex F being Function st ( F . 0 = KX & F . n = b2 & dom F = NAT & ( for k being Nat for KX1 being SimplicialComplexStr of X st KX1 = F . k holds F . (k + 1) = subdivision (P,KX1) ) ) holds b1 = b2 proofend; end; :: 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 b5 being SimplicialComplexStr of X holds ( b5 = subdivision (n,P,KX) iff ex F being Function st ( F . 0 = KX & F . n = b5 & dom F = NAT & ( for k being Nat for KX1 being SimplicialComplexStr of X st KX1 = F . k holds F . (k + 1) = subdivision (P,KX1) ) ) ); theorem Th61: :: SIMPLEX0:61 for X being set for KX being SimplicialComplexStr of X for P being Function holds subdivision (0,P,KX) = KX proofend; theorem Th62: :: SIMPLEX0:62 for X being set for KX being SimplicialComplexStr of X for P being Function holds subdivision (1,P,KX) = subdivision (P,KX) proofend; theorem Th63: :: SIMPLEX0:63 for X being set for KX being SimplicialComplexStr of X for P being Function for n, k being Element of NAT holds subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX))) proofend; theorem :: SIMPLEX0:64 for X being set for n being Nat for KX being SimplicialComplexStr of X for P being Function holds [#] (subdivision (n,P,KX)) = [#] KX proofend; theorem :: SIMPLEX0:65 for X being set for n being Nat for KX being SimplicialComplexStr of X for SX being SubSimplicialComplex of KX for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX) proofend;