:: TRIANG_1 semantic presentation begin registration let X be non empty set ; let R be Order of X; cluster RelStr(# X,R #) -> non empty ; coherence not RelStr(# X,R #) is empty ; end; theorem :: TRIANG_1:1 for A being set holds {} |_2 A = {} ; theorem :: TRIANG_1:2 for F being non empty Poset for A being Subset of F st A is finite & A <> {} & ( for B, C being Element of F st B in A & C in A & not B <= C holds C <= B ) holds ex m being Element of F st ( m in A & ( for C being Element of F st C in A holds m <= C ) ) proof let F be non empty Poset; ::_thesis: for A being Subset of F st A is finite & A <> {} & ( for B, C being Element of F st B in A & C in A & not B <= C holds C <= B ) holds ex m being Element of F st ( m in A & ( for C being Element of F st C in A holds m <= C ) ) defpred S1[ set ] means ( \$1 <> {} implies ex m being Element of F st ( m in \$1 & ( for C being Element of F st C in \$1 holds m <= C ) ) ); let A be Subset of F; ::_thesis: ( A is finite & A <> {} & ( for B, C being Element of F st B in A & C in A & not B <= C holds C <= B ) implies ex m being Element of F st ( m in A & ( for C being Element of F st C in A holds m <= C ) ) ) assume that A1: A is finite and A2: A <> {} and A3: for B, C being Element of F st B in A & C in A & not B <= C holds C <= B ; ::_thesis: ex m being Element of F st ( m in A & ( for C being Element of F st C in A holds m <= C ) ) A4: now__::_thesis:_for_x_being_Element_of_F for_B_being_Subset_of_F_st_x_in_A_&_B_c=_A_&_S1[B]_holds_ S1[B_\/_{x}] let x be Element of F; ::_thesis: for B being Subset of F st x in A & B c= A & S1[B] holds S1[B \/ {x}] let B be Subset of F; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] ) assume that A5: x in A and A6: B c= A and A7: S1[B] ; ::_thesis: S1[B \/ {x}] reconsider x9 = x as Element of F ; now__::_thesis:_(_B_\/_{x}_<>_{}_implies_ex_m_being_Element_of_F_st_ (_m_in_B_\/_{x}_&_(_for_C_being_Element_of_F_st_C_in_B_\/_{x}_holds_ m_<=_C_)_)_) percases ( for y being Element of F holds ( not y in B or not y <= x9 ) or ex y being Element of F st ( y in B & y <= x9 ) ) ; supposeA8: for y being Element of F holds ( not y in B or not y <= x9 ) ; ::_thesis: ( B \/ {x} <> {} implies ex m being Element of F st ( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds m <= C ) ) ) assume B \/ {x} <> {} ; ::_thesis: ex m being Element of F st ( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds m <= C ) ) take m = x9; ::_thesis: ( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds m <= C ) ) x in {x} by TARSKI:def_1; hence m in B \/ {x} by XBOOLE_0:def_3; ::_thesis: for C being Element of F st C in B \/ {x} holds m <= C let C be Element of F; ::_thesis: ( C in B \/ {x} implies m <= C ) assume C in B \/ {x} ; ::_thesis: m <= C then A9: ( C in B or C in {x} ) by XBOOLE_0:def_3; then ( not C <= x9 or C = x ) by A8, TARSKI:def_1; hence m <= C by A3, A5, A6, A9, TARSKI:def_1; ::_thesis: verum end; supposeA10: ex y being Element of F st ( y in B & y <= x9 ) ; ::_thesis: ( B \/ {x} <> {} implies ex m being Element of F st ( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds m <= C ) ) ) assume B \/ {x} <> {} ; ::_thesis: ex m being Element of F st ( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds m <= C ) ) consider y being Element of F such that A11: y in B and A12: y <= x9 by A10; consider m being Element of F such that A13: m in B and A14: for C being Element of F st C in B holds m <= C by A7, A11; take m = m; ::_thesis: ( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds m <= C ) ) thus m in B \/ {x} by A13, XBOOLE_0:def_3; ::_thesis: for C being Element of F st C in B \/ {x} holds m <= C let C be Element of F; ::_thesis: ( C in B \/ {x} implies m <= C ) assume C in B \/ {x} ; ::_thesis: m <= C then A15: ( C in B or C in {x} ) by XBOOLE_0:def_3; m <= y by A11, A14; then m <= x9 by A12, ORDERS_2:3; hence m <= C by A14, A15, TARSKI:def_1; ::_thesis: verum end; end; end; hence S1[B \/ {x}] ; ::_thesis: verum end; A16: S1[ {} the carrier of F] ; S1[A] from PRE_POLY:sch_2(A1, A16, A4); hence ex m being Element of F st ( m in A & ( for C being Element of F st C in A holds m <= C ) ) by A2; ::_thesis: verum end; registration let P be non empty Poset; let A be non empty finite Subset of P; let x be Element of P; cluster InitSegm (A,x) -> finite ; coherence InitSegm (A,x) is finite ; end; begin definition let C be non empty Poset; func symplexes C -> Subset of (Fin the carrier of C) equals :: TRIANG_1:def 1 { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ; coherence { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } is Subset of (Fin the carrier of C) proof set S = { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ; { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } c= Fin the carrier of C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } or x in Fin the carrier of C ) assume x in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ; ::_thesis: x in Fin the carrier of C then ex a being Element of Fin the carrier of C st ( x = a & the InternalRel of C linearly_orders a ) ; hence x in Fin the carrier of C ; ::_thesis: verum end; hence { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } is Subset of (Fin the carrier of C) ; ::_thesis: verum end; end; :: deftheorem defines symplexes TRIANG_1:def_1_:_ for C being non empty Poset holds symplexes C = { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ; registration let C be non empty Poset; cluster symplexes C -> with_non-empty_element ; coherence not symplexes C is empty-membered proof set x = the Element of C; reconsider a = { the Element of C} as Element of Fin the carrier of C by FINSUB_1:def_5; A1: the InternalRel of C is_connected_in a proof let k, l be set ; :: according to RELAT_2:def_6 ::_thesis: ( not k in a or not l in a or k = l or [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) assume that A2: k in a and A3: l in a and A4: k <> l ; ::_thesis: ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) k = the Element of C by A2, TARSKI:def_1; hence ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) by A3, A4, TARSKI:def_1; ::_thesis: verum end; A5: field the InternalRel of C = the carrier of C by ORDERS_1:12; then the InternalRel of C is_antisymmetric_in the carrier of C by RELAT_2:def_12; then A6: the InternalRel of C is_antisymmetric_in a by ORDERS_1:9; the InternalRel of C is_transitive_in the carrier of C by A5, RELAT_2:def_16; then A7: the InternalRel of C is_transitive_in a by ORDERS_1:10; the InternalRel of C is_reflexive_in the carrier of C by A5, RELAT_2:def_9; then the InternalRel of C is_reflexive_in a by ORDERS_1:8; then the InternalRel of C linearly_orders a by A6, A7, A1, ORDERS_1:def_8; then a in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ; hence not symplexes C is empty-membered by SETFAM_1:def_10; ::_thesis: verum end; end; theorem Th3: :: TRIANG_1:3 for C being non empty Poset for x being Element of C holds {x} in symplexes C proof let C be non empty Poset; ::_thesis: for x being Element of C holds {x} in symplexes C let x be Element of C; ::_thesis: {x} in symplexes C reconsider a = {x} as Element of Fin the carrier of C by FINSUB_1:def_5; A1: the InternalRel of C is_connected_in a proof let k, l be set ; :: according to RELAT_2:def_6 ::_thesis: ( not k in a or not l in a or k = l or [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) assume that A2: k in a and A3: l in a and A4: k <> l ; ::_thesis: ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) k = x by A2, TARSKI:def_1; hence ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) by A3, A4, TARSKI:def_1; ::_thesis: verum end; A5: field the InternalRel of C = the carrier of C by ORDERS_1:12; then the InternalRel of C is_antisymmetric_in the carrier of C by RELAT_2:def_12; then A6: the InternalRel of C is_antisymmetric_in a by ORDERS_1:9; the InternalRel of C is_transitive_in the carrier of C by A5, RELAT_2:def_16; then A7: the InternalRel of C is_transitive_in a by ORDERS_1:10; the InternalRel of C is_reflexive_in the carrier of C by A5, RELAT_2:def_9; then the InternalRel of C is_reflexive_in a by ORDERS_1:8; then the InternalRel of C linearly_orders a by A6, A7, A1, ORDERS_1:def_8; hence {x} in symplexes C ; ::_thesis: verum end; theorem :: TRIANG_1:4 for C being non empty Poset holds {} in symplexes C proof let C be non empty Poset; ::_thesis: {} in symplexes C A1: {} is Subset of C by SUBSET_1:1; then reconsider a = {} as Element of Fin the carrier of C by FINSUB_1:def_5; A2: field the InternalRel of C = the carrier of C by ORDERS_1:12; then the InternalRel of C is_antisymmetric_in the carrier of C by RELAT_2:def_12; then A3: the InternalRel of C is_antisymmetric_in a by A1, ORDERS_1:9; A4: the InternalRel of C is_connected_in a proof let k, l be set ; :: according to RELAT_2:def_6 ::_thesis: ( not k in a or not l in a or k = l or [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) assume that A5: k in a and l in a and k <> l ; ::_thesis: ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) thus ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) by A5; ::_thesis: verum end; the InternalRel of C is_transitive_in the carrier of C by A2, RELAT_2:def_16; then A6: the InternalRel of C is_transitive_in a by A1, ORDERS_1:10; the InternalRel of C is_reflexive_in the carrier of C by A2, RELAT_2:def_9; then the InternalRel of C is_reflexive_in a by A1, ORDERS_1:8; then the InternalRel of C linearly_orders a by A3, A6, A4, ORDERS_1:def_8; hence {} in symplexes C ; ::_thesis: verum end; theorem Th5: :: TRIANG_1:5 for C being non empty Poset for x, s being set st x c= s & s in symplexes C holds x in symplexes C proof let C be non empty Poset; ::_thesis: for x, s being set st x c= s & s in symplexes C holds x in symplexes C let x, s be set ; ::_thesis: ( x c= s & s in symplexes C implies x in symplexes C ) assume that A1: x c= s and A2: s in symplexes C ; ::_thesis: x in symplexes C consider s1 being Element of Fin the carrier of C such that A3: s1 = s and A4: the InternalRel of C linearly_orders s1 by A2; s1 c= the carrier of C by FINSUB_1:def_5; then x c= the carrier of C by A1, A3, XBOOLE_1:1; then reconsider x1 = x as Element of Fin the carrier of C by A1, A2, FINSUB_1:def_5; the InternalRel of C linearly_orders x by A1, A3, A4, ORDERS_1:38; then x1 in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ; hence x in symplexes C ; ::_thesis: verum end; theorem Th6: :: TRIANG_1:6 for n being Element of NAT for C being non empty Poset for A being non empty Element of symplexes C st card A = n holds dom (SgmX ( the InternalRel of C,A)) = Seg n proof let n be Element of NAT ; ::_thesis: for C being non empty Poset for A being non empty Element of symplexes C st card A = n holds dom (SgmX ( the InternalRel of C,A)) = Seg n let C be non empty Poset; ::_thesis: for A being non empty Element of symplexes C st card A = n holds dom (SgmX ( the InternalRel of C,A)) = Seg n let A be non empty Element of symplexes C; ::_thesis: ( card A = n implies dom (SgmX ( the InternalRel of C,A)) = Seg n ) set f = SgmX ( the InternalRel of C,A); A in { A1 where A1 is Element of Fin the carrier of C : the InternalRel of C linearly_orders A1 } ; then A1: ex A1 being Element of Fin the carrier of C st ( A1 = A & the InternalRel of C linearly_orders A1 ) ; assume card A = n ; ::_thesis: dom (SgmX ( the InternalRel of C,A)) = Seg n then len (SgmX ( the InternalRel of C,A)) = n by A1, PRE_POLY:11; hence dom (SgmX ( the InternalRel of C,A)) = Seg n by FINSEQ_1:def_3; ::_thesis: verum end; registration let C be non empty Poset; cluster non empty finite for Element of symplexes C; existence not for b1 being Element of symplexes C holds b1 is empty proof set x = the Element of C; { the Element of C} in symplexes C by Th3; hence not for b1 being Element of symplexes C holds b1 is empty ; ::_thesis: verum end; end; begin definition mode SetSequence is ManySortedSet of NAT ; end; definition let IT be SetSequence; attrIT is lower_non-empty means :Def2: :: TRIANG_1:def 2 for n being Nat st not IT . n is empty holds for m being Nat st m < n holds not IT . m is empty ; end; :: deftheorem Def2 defines lower_non-empty TRIANG_1:def_2_:_ for IT being SetSequence holds ( IT is lower_non-empty iff for n being Nat st not IT . n is empty holds for m being Nat st m < n holds not IT . m is empty ); registration cluster Relation-like NAT -defined Function-like total lower_non-empty for set ; existence ex b1 being SetSequence st b1 is lower_non-empty proof set f = NAT --> 1; reconsider f = NAT --> 1 as ManySortedSet of NAT ; take f ; ::_thesis: f is lower_non-empty for n being Nat st not f . n is empty holds for m being Nat st m < n holds not f . m is empty proof let n be Nat; ::_thesis: ( not f . n is empty implies for m being Nat st m < n holds not f . m is empty ) assume not f . n is empty ; ::_thesis: for m being Nat st m < n holds not f . m is empty let m be Nat; ::_thesis: ( m < n implies not f . m is empty ) assume m < n ; ::_thesis: not f . m is empty m in NAT by ORDINAL1:def_12; hence not f . m is empty by FUNCOP_1:7; ::_thesis: verum end; hence f is lower_non-empty by Def2; ::_thesis: verum end; end; definition let X be SetSequence; func FuncsSeq X -> SetSequence means :Def3: :: TRIANG_1:def 3 for n being Nat holds it . n = Funcs ((X . (n + 1)),(X . n)); existence ex b1 being SetSequence st for n being Nat holds b1 . n = Funcs ((X . (n + 1)),(X . n)) proof deffunc H1( Element of NAT ) -> set = Funcs ((X . (\$1 + 1)),(X . \$1)); consider f being ManySortedSet of NAT such that A1: for n being Element of NAT holds f . n = H1(n) from PBOOLE:sch_5(); reconsider f = f as SetSequence ; take f ; ::_thesis: for n being Nat holds f . n = Funcs ((X . (n + 1)),(X . n)) let n be Nat; ::_thesis: f . n = Funcs ((X . (n + 1)),(X . n)) n in NAT by ORDINAL1:def_12; hence f . n = Funcs ((X . (n + 1)),(X . n)) by A1; ::_thesis: verum end; uniqueness for b1, b2 being SetSequence st ( for n being Nat holds b1 . n = Funcs ((X . (n + 1)),(X . n)) ) & ( for n being Nat holds b2 . n = Funcs ((X . (n + 1)),(X . n)) ) holds b1 = b2 proof let a, b be SetSequence; ::_thesis: ( ( for n being Nat holds a . n = Funcs ((X . (n + 1)),(X . n)) ) & ( for n being Nat holds b . n = Funcs ((X . (n + 1)),(X . n)) ) implies a = b ) assume that A2: for n being Nat holds a . n = Funcs ((X . (n + 1)),(X . n)) and A3: for n being Nat holds b . n = Funcs ((X . (n + 1)),(X . n)) ; ::_thesis: a = b let n be Element of NAT ; :: according to PBOOLE:def_21 ::_thesis: a . n = b . n a . n = Funcs ((X . (n + 1)),(X . n)) by A2; hence a . n c= b . n by A3; :: according to XBOOLE_0:def_10 ::_thesis: b . n c= a . n a . n = Funcs ((X . (n + 1)),(X . n)) by A2; hence b . n c= a . n by A3; ::_thesis: verum end; end; :: deftheorem Def3 defines FuncsSeq TRIANG_1:def_3_:_ for X, b2 being SetSequence holds ( b2 = FuncsSeq X iff for n being Nat holds b2 . n = Funcs ((X . (n + 1)),(X . n)) ); registration let X be lower_non-empty SetSequence; let n be Nat; cluster(FuncsSeq X) . n -> non empty ; coherence not (FuncsSeq X) . n is empty proof n < n + 1 by NAT_1:13; then A1: ( X . (n + 1) = {} or X . n <> {} ) by Def2; (FuncsSeq X) . n = Funcs ((X . (n + 1)),(X . n)) by Def3; hence not (FuncsSeq X) . n is empty by A1, FUNCT_2:8; ::_thesis: verum end; end; definition let n be Nat; let f be Element of Funcs ((Seg n),(Seg (n + 1))); func @ f -> FinSequence of REAL equals :: TRIANG_1:def 4 f; coherence f is FinSequence of REAL proof consider x being Function such that A1: x = f and dom x = Seg n and rng x c= Seg (n + 1) by FUNCT_2:def_2; reconsider x = x as FinSequence of Seg (n + 1) by A1, FINSEQ_2:25; Seg (n + 1) c= REAL by XBOOLE_1:1; then x is FinSequence of REAL by FINSEQ_2:24; hence f is FinSequence of REAL by A1; ::_thesis: verum end; end; :: deftheorem defines @ TRIANG_1:def_4_:_ for n being Nat for f being Element of Funcs ((Seg n),(Seg (n + 1))) holds @ f = f; definition func NatEmbSeq -> SetSequence means :Def5: :: TRIANG_1:def 5 for n being Nat holds it . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ; existence ex b1 being SetSequence st for n being Nat holds b1 . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } proof deffunc H1( Element of NAT ) -> set = { f where f is Element of Funcs ((Seg \$1),(Seg (\$1 + 1))) : @ f is increasing } ; consider F being ManySortedSet of NAT such that A1: for n being Element of NAT holds F . n = H1(n) from PBOOLE:sch_5(); reconsider F = F as SetSequence ; take F ; ::_thesis: for n being Nat holds F . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } let n be Nat; ::_thesis: F . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } n in NAT by ORDINAL1:def_12; hence F . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A1; ::_thesis: verum end; uniqueness for b1, b2 being SetSequence st ( for n being Nat holds b1 . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ) & ( for n being Nat holds b2 . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ) holds b1 = b2 proof let a, b be SetSequence; ::_thesis: ( ( for n being Nat holds a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ) & ( for n being Nat holds b . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ) implies a = b ) assume that A2: for n being Nat holds a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } and A3: for n being Nat holds b . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ; ::_thesis: a = b let n be Element of NAT ; :: according to PBOOLE:def_21 ::_thesis: a . n = b . n a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A2; hence a . n c= b . n by A3; :: according to XBOOLE_0:def_10 ::_thesis: b . n c= a . n a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A2; hence b . n c= a . n by A3; ::_thesis: verum end; end; :: deftheorem Def5 defines NatEmbSeq TRIANG_1:def_5_:_ for b1 being SetSequence holds ( b1 = NatEmbSeq iff for n being Nat holds b1 . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ); registration let n be Nat; clusterNatEmbSeq . n -> non empty ; coherence not NatEmbSeq . n is empty proof n <= n + 1 by NAT_1:11; then A1: Seg n c= Seg (n + 1) by FINSEQ_1:5; A2: rng (id (Seg n)) = Seg n ; dom (id (Seg n)) = Seg n ; then reconsider n1 = idseq n as Element of Funcs ((Seg n),(Seg (n + 1))) by A1, A2, FUNCT_2:def_2; @ n1 is increasing ; then n1 in { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ; hence not NatEmbSeq . n is empty by Def5; ::_thesis: verum end; end; registration let n be Nat; cluster -> Relation-like Function-like for Element of NatEmbSeq . n; coherence for b1 being Element of NatEmbSeq . n holds ( b1 is Function-like & b1 is Relation-like ) proof reconsider n9 = n as Element of NAT by ORDINAL1:def_12; let x be Element of NatEmbSeq . n; ::_thesis: ( x is Function-like & x is Relation-like ) A1: x in NatEmbSeq . n9 ; NatEmbSeq . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by Def5; then ex f being Element of Funcs ((Seg n),(Seg (n + 1))) st ( x = f & @ f is increasing ) by A1; hence ( x is Function-like & x is Relation-like ) ; ::_thesis: verum end; end; definition let X be SetSequence; mode triangulation of X is ManySortedFunction of NatEmbSeq , FuncsSeq X; end; definition attrc1 is strict ; struct TriangStr -> ; aggrTriangStr(# SkeletonSeq, FacesAssign #) -> TriangStr ; sel SkeletonSeq c1 -> SetSequence; sel FacesAssign c1 -> ManySortedFunction of NatEmbSeq , FuncsSeq the SkeletonSeq of c1; end; definition let T be TriangStr ; attrT is lower_non-empty means :Def6: :: TRIANG_1:def 6 the SkeletonSeq of T is lower_non-empty ; end; :: deftheorem Def6 defines lower_non-empty TRIANG_1:def_6_:_ for T being TriangStr holds ( T is lower_non-empty iff the SkeletonSeq of T is lower_non-empty ); registration cluster strict lower_non-empty for TriangStr ; existence ex b1 being TriangStr st ( b1 is lower_non-empty & b1 is strict ) proof set Sk = NAT --> {}; reconsider Sk = NAT --> {} as ManySortedSet of NAT ; set A = the ManySortedFunction of NatEmbSeq , FuncsSeq Sk; take TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) ; ::_thesis: ( TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is lower_non-empty & TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is strict ) for n being Nat st not Sk . n is empty holds for m being Nat st m < n holds not Sk . m is empty proof let n be Nat; ::_thesis: ( not Sk . n is empty implies for m being Nat st m < n holds not Sk . m is empty ) assume A1: not Sk . n is empty ; ::_thesis: for m being Nat st m < n holds not Sk . m is empty n in NAT by ORDINAL1:def_12; hence for m being Nat st m < n holds not Sk . m is empty by A1, FUNCOP_1:7; ::_thesis: verum end; then Sk is lower_non-empty by Def2; hence ( TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is lower_non-empty & TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is strict ) by Def6; ::_thesis: verum end; end; registration let T be lower_non-empty TriangStr ; cluster the SkeletonSeq of T -> lower_non-empty ; coherence the SkeletonSeq of T is lower_non-empty by Def6; end; registration let S be lower_non-empty SetSequence; let F be ManySortedFunction of NatEmbSeq , FuncsSeq S; cluster TriangStr(# S,F #) -> lower_non-empty ; coherence TriangStr(# S,F #) is lower_non-empty by Def6; end; begin definition let T be TriangStr ; let n be Nat; mode Symplex of T,n is Element of the SkeletonSeq of T . n; end; definition let n be Nat; mode Face of n is Element of NatEmbSeq . n; end; definition let T be lower_non-empty TriangStr ; let n be Nat; let x be Symplex of T,(n + 1); let f be Face of n; assume A1: the SkeletonSeq of T . (n + 1) <> {} ; func face (x,f) -> Symplex of T,n means :Def7: :: TRIANG_1:def 7 for F, G being Function st F = the FacesAssign of T . n & G = F . f holds it = G . x; existence ex b1 being Symplex of T,n st for F, G being Function st F = the FacesAssign of T . n & G = F . f holds b1 = G . x proof reconsider n9 = n as Element of NAT by ORDINAL1:def_12; reconsider F = the FacesAssign of T . n9 as Function of (NatEmbSeq . n9),((FuncsSeq the SkeletonSeq of T) . n9) by PBOOLE:def_15; F . f in (FuncsSeq the SkeletonSeq of T) . n9 by FUNCT_2:5; then F . f in Funcs (( the SkeletonSeq of T . (n + 1)),( the SkeletonSeq of T . n)) by Def3; then consider G being Function such that A2: G = F . f and A3: dom G = the SkeletonSeq of T . (n + 1) and A4: rng G c= the SkeletonSeq of T . n by FUNCT_2:def_2; G . x in rng G by A1, A3, FUNCT_1:def_3; then reconsider S = G . x as Symplex of T,n by A4; take S ; ::_thesis: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds S = G . x let F1, G1 be Function; ::_thesis: ( F1 = the FacesAssign of T . n & G1 = F1 . f implies S = G1 . x ) assume that A5: F1 = the FacesAssign of T . n and A6: G1 = F1 . f ; ::_thesis: S = G1 . x thus S = G1 . x by A2, A5, A6; ::_thesis: verum end; uniqueness for b1, b2 being Symplex of T,n st ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds b1 = G . x ) & ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds b2 = G . x ) holds b1 = b2 proof reconsider n9 = n as Element of NAT by ORDINAL1:def_12; let S1, S2 be Symplex of T,n; ::_thesis: ( ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds S1 = G . x ) & ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds S2 = G . x ) implies S1 = S2 ) assume that A7: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds S1 = G . x and A8: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds S2 = G . x ; ::_thesis: S1 = S2 reconsider F = the FacesAssign of T . n9 as Function of (NatEmbSeq . n9),((FuncsSeq the SkeletonSeq of T) . n9) by PBOOLE:def_15; F . f in (FuncsSeq the SkeletonSeq of T) . n9 by FUNCT_2:5; then F . f in Funcs (( the SkeletonSeq of T . (n + 1)),( the SkeletonSeq of T . n)) by Def3; then consider G being Function such that A9: G = F . f and dom G = the SkeletonSeq of T . (n + 1) and rng G c= the SkeletonSeq of T . n by FUNCT_2:def_2; S1 = G . x by A7, A9; hence S1 = S2 by A8, A9; ::_thesis: verum end; end; :: deftheorem Def7 defines face TRIANG_1:def_7_:_ for T being lower_non-empty TriangStr for n being Nat for x being Symplex of T,(n + 1) for f being Face of n st the SkeletonSeq of T . (n + 1) <> {} holds for b5 being Symplex of T,n holds ( b5 = face (x,f) iff for F, G being Function st F = the FacesAssign of T . n & G = F . f holds b5 = G . x ); definition let C be non empty Poset; func Triang C -> strict lower_non-empty TriangStr means :: TRIANG_1:def 8 ( the SkeletonSeq of it . 0 = {{}} & ( for n being Nat st n > 0 holds the SkeletonSeq of it . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat for f being Face of n for s being Element of the SkeletonSeq of it . (n + 1) st s in the SkeletonSeq of it . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) ); existence ex b1 being strict lower_non-empty TriangStr st ( the SkeletonSeq of b1 . 0 = {{}} & ( for n being Nat st n > 0 holds the SkeletonSeq of b1 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat for f being Face of n for s being Element of the SkeletonSeq of b1 . (n + 1) st s in the SkeletonSeq of b1 . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) ) proof deffunc H1( Element of NAT ) -> set = IFEQ (\$1,0,{{}}, { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = \$1 } ); consider Sk being SetSequence such that A1: for n being Element of NAT holds Sk . n = H1(n) from PBOOLE:sch_5(); A2: now__::_thesis:_for_n_being_Nat_st_n_<>_0_holds_ Sk_._n_=__{__(SgmX_(_the_InternalRel_of_C,s))_where_s_is_non_empty_Element_of_symplexes_C_:_card_s_=_n__}_ let n be Nat; ::_thesis: ( n <> 0 implies Sk . n = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } ) assume A3: n <> 0 ; ::_thesis: Sk . n = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } n in NAT by ORDINAL1:def_12; hence Sk . n = IFEQ (n,0,{{}}, { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } ) by A1 .= { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } by A3, FUNCOP_1:def_8 ; ::_thesis: verum end; A4: Sk . 0 = IFEQ (0,0,{{}}, { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = 0 } ) by A1 .= {{}} by FUNCOP_1:def_8 ; Sk is lower_non-empty proof defpred S1[ Nat] means not Sk . \$1 is empty ; let n be Nat; :: according to TRIANG_1:def_2 ::_thesis: ( not Sk . n is empty implies for m being Nat st m < n holds not Sk . m is empty ) A5: for m being Element of NAT st m < n & S1[m + 1] holds S1[m] proof let m be Element of NAT ; ::_thesis: ( m < n & S1[m + 1] implies S1[m] ) assume that m < n and A6: not Sk . (m + 1) is empty ; ::_thesis: S1[m] consider g being set such that A7: g in Sk . (m + 1) by A6, XBOOLE_0:def_1; Sk . (m + 1) = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = m + 1 } by A2; then consider s being non empty Element of symplexes C such that g = SgmX ( the InternalRel of C,s) and A8: card s = m + 1 by A7; set x = the Element of s; reconsider sx = s \ { the Element of s} as finite set ; sx \/ { the Element of s} = s \/ { the Element of s} by XBOOLE_1:39; then A9: sx \/ { the Element of s} = s by XBOOLE_1:12; not the Element of s in sx by ZFMISC_1:56; then A10: m + 1 = (card sx) + 1 by A8, A9, CARD_2:41; percases ( m = 0 or m <> 0 ) ; suppose m = 0 ; ::_thesis: S1[m] hence S1[m] by A4; ::_thesis: verum end; supposeA11: m <> 0 ; ::_thesis: S1[m] then reconsider sx = sx as non empty Element of symplexes C by A10, Th5, XBOOLE_1:36; SgmX ( the InternalRel of C,sx) in { (SgmX ( the InternalRel of C,s1)) where s1 is non empty Element of symplexes C : card s1 = m } by A10; hence S1[m] by A2, A11; ::_thesis: verum end; end; end; assume A12: S1[n] ; ::_thesis: for m being Nat st m < n holds not Sk . m is empty A13: for m being Element of NAT st m <= n holds S1[m] from PRE_POLY:sch_1(A12, A5); let m be Nat; ::_thesis: ( m < n implies not Sk . m is empty ) assume A14: m < n ; ::_thesis: not Sk . m is empty m in NAT by ORDINAL1:def_12; hence not Sk . m is empty by A13, A14; ::_thesis: verum end; then reconsider Sk = Sk as lower_non-empty SetSequence ; defpred S1[ set , set , set ] means ex n being Nat ex y being Face of n st ( \$2 = y & \$3 = n & ( for s being Element of Sk . (n + 1) st s in Sk . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds for g1 being Function st g1 = \$1 holds g1 . s = (SgmX ( the InternalRel of C,A)) * y ) ); A15: for i being set st i in NAT holds for x being set st x in NatEmbSeq . i holds ex y being set st ( y in (FuncsSeq Sk) . i & S1[y,x,i] ) proof let i be set ; ::_thesis: ( i in NAT implies for x being set st x in NatEmbSeq . i holds ex y being set st ( y in (FuncsSeq Sk) . i & S1[y,x,i] ) ) assume i in NAT ; ::_thesis: for x being set st x in NatEmbSeq . i holds ex y being set st ( y in (FuncsSeq Sk) . i & S1[y,x,i] ) then reconsider n = i as Element of NAT ; let x be set ; ::_thesis: ( x in NatEmbSeq . i implies ex y being set st ( y in (FuncsSeq Sk) . i & S1[y,x,i] ) ) assume A16: x in NatEmbSeq . i ; ::_thesis: ex y being set st ( y in (FuncsSeq Sk) . i & S1[y,x,i] ) then reconsider y = x as Face of n ; reconsider y1 = y as Function ; x in { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A16, Def5; then A17: ex f being Element of Funcs ((Seg n),(Seg (n + 1))) st ( f = x & @ f is increasing ) ; then consider y2 being Function such that A18: y2 = y1 and A19: dom y2 = Seg n and A20: rng y2 c= Seg (n + 1) by FUNCT_2:def_2; reconsider y2 = y2 as FinSequence by A19, FINSEQ_1:def_2; A21: len y2 = n by A19, FINSEQ_1:def_3; defpred S2[ set , set ] means ex f being Function st ( f = \$1 & \$2 = f * y1 ); A22: for s being set st s in Sk . (n + 1) holds ex u being set st S2[s,u] proof let s be set ; ::_thesis: ( s in Sk . (n + 1) implies ex u being set st S2[s,u] ) assume s in Sk . (n + 1) ; ::_thesis: ex u being set st S2[s,u] then s in { (SgmX ( the InternalRel of C,s9)) where s9 is non empty Element of symplexes C : card s9 = n + 1 } by A2; then consider A being non empty Element of symplexes C such that A23: SgmX ( the InternalRel of C,A) = s and card A = n + 1 ; reconsider u = (SgmX ( the InternalRel of C,A)) * y as set ; consider f being Function such that A24: f = s by A23; take u ; ::_thesis: S2[s,u] take f ; ::_thesis: ( f = s & u = f * y1 ) thus ( f = s & u = f * y1 ) by A23, A24; ::_thesis: verum end; consider g being Function such that A25: dom g = Sk . (n + 1) and A26: for s being set st s in Sk . (n + 1) holds S2[s,g . s] from CLASSES1:sch_1(A22); reconsider y2 = y2 as FinSequence of Seg (n + 1) by A20, FINSEQ_1:def_4; reconsider g9 = g as set ; take g9 ; ::_thesis: ( g9 in (FuncsSeq Sk) . i & S1[g9,x,i] ) A27: y2 is one-to-one proof let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in dom y2 or not b in dom y2 or not y2 . a = y2 . b or a = b ) assume that A28: a in dom y2 and A29: b in dom y2 and A30: y2 . a = y2 . b ; ::_thesis: a = b reconsider a = a, b = b as Element of NAT by A28, A29; now__::_thesis:_not_a_<>_b assume A31: a <> b ; ::_thesis: contradiction percases ( a < b or b < a ) by A31, XXREAL_0:1; suppose a < b ; ::_thesis: contradiction hence contradiction by A17, A18, A28, A29, A30, SEQM_3:def_1; ::_thesis: verum end; suppose b < a ; ::_thesis: contradiction hence contradiction by A17, A18, A28, A29, A30, SEQM_3:def_1; ::_thesis: verum end; end; end; hence a = b ; ::_thesis: verum end; rng g c= Sk . n proof reconsider F = symplexes C as with_non-empty_element Subset of (Fin the carrier of C) ; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng g or z in Sk . n ) assume z in rng g ; ::_thesis: z in Sk . n then consider a being set such that A32: a in dom g and A33: z = g . a by FUNCT_1:def_3; consider f being Function such that A34: f = a and A35: g . a = f * y2 by A18, A25, A26, A32; percases ( n = 0 or n <> 0 ) ; supposeA36: n = 0 ; ::_thesis: z in Sk . n then Seg n = {} ; then dom (f * y1) = {} by A18, A19, RELAT_1:25, XBOOLE_1:3; then z = {} by A18, A33, A35; hence z in Sk . n by A4, A36, TARSKI:def_1; ::_thesis: verum end; supposeA37: n <> 0 ; ::_thesis: z in Sk . n f in { (SgmX ( the InternalRel of C,s1)) where s1 is non empty Element of symplexes C : card s1 = n + 1 } by A2, A25, A32, A34; then consider s1 being non empty Element of symplexes C such that A38: SgmX ( the InternalRel of C,s1) = f and A39: card s1 = n + 1 ; s1 in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ; then A40: ex s19 being Element of Fin the carrier of C st ( s19 = s1 & the InternalRel of C linearly_orders s19 ) ; then rng f = s1 by A38, PRE_POLY:def_2; then reconsider f = f as FinSequence of s1 by A38, FINSEQ_1:def_4; reconsider f = f as FinSequence of RelStr(# s1,( the InternalRel of C |_2 s1) #) ; A41: f is one-to-one by A38, A40, PRE_POLY:10; A42: dom f = Seg (n + 1) by A38, A39, Th6; A43: f is Function of (dom f),s1 by FINSEQ_2:26; then f is Function of (Seg (n + 1)), the carrier of C by A42, FUNCT_2:7; then reconsider z1 = z as FinSequence of RelStr(# the carrier of C, the InternalRel of C #) by A33, A35, FINSEQ_2:32; reconsider f = f as Function of (Seg (n + 1)), the carrier of C by A42, A43, FUNCT_2:7; A44: dom (f * y2) = Seg n by A19, A20, A42, RELAT_1:27; rng (f * y2) c= the carrier of C by FINSEQ_1:def_4; then reconsider r = rng (f * y2) as Element of Fin the carrier of C by FINSUB_1:def_5; rng (f * y2) c= s1 by RELAT_1:def_19; then reconsider s9 = r as non empty Element of F by A37, A44, Th5, RELAT_1:42; for n1, m1 being Nat st n1 in dom z1 & m1 in dom z1 & n1 < m1 holds ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C ) proof let n1, m1 be Nat; ::_thesis: ( n1 in dom z1 & m1 in dom z1 & n1 < m1 implies ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C ) ) assume that A45: n1 in dom z1 and A46: m1 in dom z1 and A47: n1 < m1 ; ::_thesis: ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C ) y2 . m1 in Seg (n + 1) by A19, A33, A35, A44, A46, FINSEQ_2:11; then reconsider ym = y2 . m1 as Element of NAT ; y2 . n1 in Seg (n + 1) by A19, A33, A35, A44, A45, FINSEQ_2:11; then reconsider yn = y2 . n1 as Element of NAT ; A48: yn < ym by A17, A18, A19, A33, A35, A44, A45, A46, A47, SEQM_3:def_1; A49: ym in rng y2 by A19, A33, A35, A44, A46, FUNCT_1:def_3; then reconsider fm = f . ym as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) by A20, A42, FINSEQ_2:11; A50: fm = f /. ym by A20, A42, A49, PARTFUN1:def_6; z1 . m1 = fm by A33, A35, A46, FUNCT_1:12; then reconsider zm = z1 . m1 as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) ; A51: zm = z1 /. m1 by A46, PARTFUN1:def_6; A52: z1 . m1 = f . (y2 . m1) by A33, A35, A46, FUNCT_1:12; A53: z1 . n1 = f . (y2 . n1) by A33, A35, A45, FUNCT_1:12; A54: yn in rng y2 by A19, A33, A35, A44, A45, FUNCT_1:def_3; then reconsider fn = f . yn as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) by A20, A42, FINSEQ_2:11; z1 . n1 = fn by A33, A35, A45, FUNCT_1:12; then reconsider zn = z1 . n1 as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) ; A55: zn = z1 /. n1 by A45, PARTFUN1:def_6; fn = f /. yn by A20, A42, A54, PARTFUN1:def_6; hence ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C ) by A20, A38, A40, A42, A53, A52, A48, A54, A49, A50, A55, A51, PRE_POLY:def_2; ::_thesis: verum end; then A56: z1 = SgmX ( the InternalRel of C,s9) by A33, A35, PRE_POLY:9; len (f * y2) = n by A20, A21, A42, FINSEQ_2:29; then card s9 = n by A27, A41, FINSEQ_4:62; then z in { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } by A56; hence z in Sk . n by A2, A37; ::_thesis: verum end; end; end; then g9 in Funcs ((Sk . (n + 1)),(Sk . n)) by A25, FUNCT_2:def_2; hence g9 in (FuncsSeq Sk) . i by Def3; ::_thesis: S1[g9,x,i] reconsider y = x as Face of n by A16; take n ; ::_thesis: ex y being Face of n st ( x = y & i = n & ( for s being Element of Sk . (n + 1) st s in Sk . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds for g1 being Function st g1 = g9 holds g1 . s = (SgmX ( the InternalRel of C,A)) * y ) ) take y ; ::_thesis: ( x = y & i = n & ( for s being Element of Sk . (n + 1) st s in Sk . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds for g1 being Function st g1 = g9 holds g1 . s = (SgmX ( the InternalRel of C,A)) * y ) ) thus ( x = y & i = n ) ; ::_thesis: for s being Element of Sk . (n + 1) st s in Sk . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds for g1 being Function st g1 = g9 holds g1 . s = (SgmX ( the InternalRel of C,A)) * y let s be Element of Sk . (n + 1); ::_thesis: ( s in Sk . (n + 1) implies for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds for g1 being Function st g1 = g9 holds g1 . s = (SgmX ( the InternalRel of C,A)) * y ) assume s in Sk . (n + 1) ; ::_thesis: for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds for g1 being Function st g1 = g9 holds g1 . s = (SgmX ( the InternalRel of C,A)) * y then A57: ex f being Function st ( f = s & g . s = f * y1 ) by A26; let A be non empty Element of symplexes C; ::_thesis: ( SgmX ( the InternalRel of C,A) = s implies for g1 being Function st g1 = g9 holds g1 . s = (SgmX ( the InternalRel of C,A)) * y ) assume A58: SgmX ( the InternalRel of C,A) = s ; ::_thesis: for g1 being Function st g1 = g9 holds g1 . s = (SgmX ( the InternalRel of C,A)) * y let g1 be Function; ::_thesis: ( g1 = g9 implies g1 . s = (SgmX ( the InternalRel of C,A)) * y ) assume g1 = g9 ; ::_thesis: g1 . s = (SgmX ( the InternalRel of C,A)) * y hence g1 . s = (SgmX ( the InternalRel of C,A)) * y by A58, A57; ::_thesis: verum end; consider F being ManySortedFunction of NatEmbSeq , FuncsSeq Sk such that A59: for i being set st i in NAT holds ex f being Function of (NatEmbSeq . i),((FuncsSeq Sk) . i) st ( f = F . i & ( for x being set st x in NatEmbSeq . i holds S1[f . x,x,i] ) ) from MSSUBFAM:sch_1(A15); take TriangStr(# Sk,F #) ; ::_thesis: ( the SkeletonSeq of TriangStr(# Sk,F #) . 0 = {{}} & ( for n being Nat st n > 0 holds the SkeletonSeq of TriangStr(# Sk,F #) . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat for f being Face of n for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) ) thus the SkeletonSeq of TriangStr(# Sk,F #) . 0 = {{}} by A4; ::_thesis: ( ( for n being Nat st n > 0 holds the SkeletonSeq of TriangStr(# Sk,F #) . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat for f being Face of n for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) ) thus for n being Nat st n > 0 holds the SkeletonSeq of TriangStr(# Sk,F #) . n = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } by A2; ::_thesis: for n being Nat for f being Face of n for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f let n be Nat; ::_thesis: for f being Face of n for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f n in NAT by ORDINAL1:def_12; then consider f1 being Function of (NatEmbSeq . n),((FuncsSeq Sk) . n) such that A60: f1 = F . n and A61: for x being set st x in NatEmbSeq . n holds ex m being Nat ex y being Face of m st ( x = y & n = m & ( for s being Element of Sk . (m + 1) st s in Sk . (m + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds for g1 being Function st g1 = f1 . x holds g1 . s = (SgmX ( the InternalRel of C,A)) * y ) ) by A59; let x be Face of n; ::_thesis: for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,x) = (SgmX ( the InternalRel of C,A)) * x let s be Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1); ::_thesis: ( s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) implies for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,x) = (SgmX ( the InternalRel of C,A)) * x ) assume A62: s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) ; ::_thesis: for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,x) = (SgmX ( the InternalRel of C,A)) * x let A be non empty Element of symplexes C; ::_thesis: ( SgmX ( the InternalRel of C,A) = s implies face (s,x) = (SgmX ( the InternalRel of C,A)) * x ) assume A63: SgmX ( the InternalRel of C,A) = s ; ::_thesis: face (s,x) = (SgmX ( the InternalRel of C,A)) * x A64: ex m being Nat ex y being Face of m st ( x = y & n = m & ( for s being Element of Sk . (m + 1) st s in Sk . (m + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds for g1 being Function st g1 = f1 . x holds g1 . s = (SgmX ( the InternalRel of C,A)) * y ) ) by A61; f1 . x in (FuncsSeq Sk) . n ; then f1 . x in Funcs ((Sk . (n + 1)),(Sk . n)) by Def3; then consider G being Function such that A65: f1 . x = G and dom G = Sk . (n + 1) and rng G c= Sk . n by FUNCT_2:def_2; face (s,x) = G . s by A60, A62, A65, Def7; hence face (s,x) = (SgmX ( the InternalRel of C,A)) * x by A62, A63, A64, A65; ::_thesis: verum end; uniqueness for b1, b2 being strict lower_non-empty TriangStr st the SkeletonSeq of b1 . 0 = {{}} & ( for n being Nat st n > 0 holds the SkeletonSeq of b1 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat for f being Face of n for s being Element of the SkeletonSeq of b1 . (n + 1) st s in the SkeletonSeq of b1 . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) & the SkeletonSeq of b2 . 0 = {{}} & ( for n being Nat st n > 0 holds the SkeletonSeq of b2 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat for f being Face of n for s being Element of the SkeletonSeq of b2 . (n + 1) st s in the SkeletonSeq of b2 . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) holds b1 = b2 proof let T1, T2 be strict lower_non-empty TriangStr ; ::_thesis: ( the SkeletonSeq of T1 . 0 = {{}} & ( for n being Nat st n > 0 holds the SkeletonSeq of T1 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat for f being Face of n for s being Element of the SkeletonSeq of T1 . (n + 1) st s in the SkeletonSeq of T1 . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) & the SkeletonSeq of T2 . 0 = {{}} & ( for n being Nat st n > 0 holds the SkeletonSeq of T2 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat for f being Face of n for s being Element of the SkeletonSeq of T2 . (n + 1) st s in the SkeletonSeq of T2 . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) implies T1 = T2 ) assume that A66: the SkeletonSeq of T1 . 0 = {{}} and A67: for n being Nat st n > 0 holds the SkeletonSeq of T1 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } and A68: for n being Nat for f being Face of n for s being Element of the SkeletonSeq of T1 . (n + 1) st s in the SkeletonSeq of T1 . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f and A69: the SkeletonSeq of T2 . 0 = {{}} and A70: for n being Nat st n > 0 holds the SkeletonSeq of T2 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } and A71: for n being Nat for f being Face of n for s being Element of the SkeletonSeq of T2 . (n + 1) st s in the SkeletonSeq of T2 . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f ; ::_thesis: T1 = T2 A72: for x being set st x in NAT holds the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x proof let x be set ; ::_thesis: ( x in NAT implies the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x ) assume x in NAT ; ::_thesis: the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x then reconsider n = x as Element of NAT ; now__::_thesis:_the_SkeletonSeq_of_T1_._n_=_the_SkeletonSeq_of_T2_._n percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n hence the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n by A66, A69; ::_thesis: verum end; supposeA73: n <> 0 ; ::_thesis: the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n then the SkeletonSeq of T1 . n = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } by A67; hence the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n by A70, A73; ::_thesis: verum end; end; end; hence the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x ; ::_thesis: verum end; then A74: the SkeletonSeq of T1 = the SkeletonSeq of T2 by PBOOLE:3; now__::_thesis:_for_i_being_set_st_i_in_NAT_holds_ the_FacesAssign_of_T1_._i_=_the_FacesAssign_of_T2_._i let i be set ; ::_thesis: ( i in NAT implies the FacesAssign of T1 . i = the FacesAssign of T2 . i ) assume i in NAT ; ::_thesis: the FacesAssign of T1 . i = the FacesAssign of T2 . i then reconsider n = i as Element of NAT ; reconsider F1n = the FacesAssign of T1 . n, F2n = the FacesAssign of T2 . n as Function of (NatEmbSeq . n),((FuncsSeq the SkeletonSeq of T1) . n) by A74, PBOOLE:def_15; A75: dom F2n = NatEmbSeq . n by FUNCT_2:def_1; A76: now__::_thesis:_for_x_being_set_st_x_in_NatEmbSeq_._n_holds_ F1n_._x_=_F2n_._x let x be set ; ::_thesis: ( x in NatEmbSeq . n implies F1n . x = F2n . x ) assume x in NatEmbSeq . n ; ::_thesis: F1n . x = F2n . x then reconsider x1 = x as Face of n ; F1n . x1 in (FuncsSeq the SkeletonSeq of T1) . n ; then F1n . x1 in Funcs (( the SkeletonSeq of T1 . (n + 1)),( the SkeletonSeq of T1 . n)) by Def3; then consider F1nx being Function such that A77: F1nx = F1n . x1 and A78: dom F1nx = the SkeletonSeq of T1 . (n + 1) and rng F1nx c= the SkeletonSeq of T1 . n by FUNCT_2:def_2; F2n . x1 in (FuncsSeq the SkeletonSeq of T1) . n ; then F2n . x1 in Funcs (( the SkeletonSeq of T1 . (n + 1)),( the SkeletonSeq of T1 . n)) by Def3; then consider F2nx being Function such that A79: F2nx = F2n . x1 and A80: dom F2nx = the SkeletonSeq of T1 . (n + 1) and rng F2nx c= the SkeletonSeq of T1 . n by FUNCT_2:def_2; now__::_thesis:_for_y_being_set_st_y_in_the_SkeletonSeq_of_T1_._(n_+_1)_holds_ F1nx_._y_=_F2nx_._y let y be set ; ::_thesis: ( y in the SkeletonSeq of T1 . (n + 1) implies F1nx . y = F2nx . y ) assume A81: y in the SkeletonSeq of T1 . (n + 1) ; ::_thesis: F1nx . y = F2nx . y then reconsider y1 = y as Symplex of T1,(n + 1) ; A82: F1nx . y1 = face (y1,x1) by A77, A81, Def7; reconsider y2 = y as Symplex of T2,(n + 1) by A72, A81; A83: F2nx . y2 = face (y2,x1) by A74, A79, A81, Def7; y1 in { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n + 1 } by A67, A81; then consider A being non empty Element of symplexes C such that A84: SgmX ( the InternalRel of C,A) = y1 and card A = n + 1 ; face (y1,x1) = (SgmX ( the InternalRel of C,A)) * x1 by A68, A81, A84; hence F1nx . y = F2nx . y by A71, A74, A81, A82, A83, A84; ::_thesis: verum end; hence F1n . x = F2n . x by A77, A78, A79, A80, FUNCT_1:2; ::_thesis: verum end; dom F1n = NatEmbSeq . n by FUNCT_2:def_1; hence the FacesAssign of T1 . i = the FacesAssign of T2 . i by A75, A76, FUNCT_1:2; ::_thesis: verum end; hence T1 = T2 by A74, PBOOLE:3; ::_thesis: verum end; end; :: deftheorem defines Triang TRIANG_1:def_8_:_ for C being non empty Poset for b2 being strict lower_non-empty TriangStr holds ( b2 = Triang C iff ( the SkeletonSeq of b2 . 0 = {{}} & ( for n being Nat st n > 0 holds the SkeletonSeq of b2 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat for f being Face of n for s being Element of the SkeletonSeq of b2 . (n + 1) st s in the SkeletonSeq of b2 . (n + 1) holds for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) ) );