environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XBOOLE_0, ORDERS_1, ORDERS_2, WELLORD1, FINSET_1, XXREAL_0, TARSKI, STRUCT_0, FINSUB_1, SETFAM_1, RELAT_2, RELAT_1, CARD_1, PRE_POLY, FINSEQ_1, PROB_1, PBOOLE, NAT_1, FUNCT_1, ARYTM_3, FUNCOP_1, FUNCT_2, QC_LANG1, ORDINAL2, FINSEQ_2, PARTFUN1, TRIANG_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1, RELAT_2, SETFAM_1, ORDERS_1, DOMAIN_1, XCMPLX_0, NAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, FINSEQ_1, FINSEQ_2, FINSUB_1, STRUCT_0, WELLORD1, SEQM_3, PBOOLE, ORDERS_2, FINSEQOP, FUNCOP_1, XXREAL_0, PRE_POLY;
definitions RELAT_2, TARSKI, FUNCT_1, XBOOLE_0, PBOOLE;
theorems RELAT_1, ORDERS_2, RELAT_2, ZFMISC_1, TARSKI, SUBSET_1, ORDERS_1, FINSUB_1, NAT_1, FUNCT_2, PBOOLE, FUNCT_1, FINSEQ_1, CARD_2, FINSEQ_4, FINSEQ_2, FUNCOP_1, SEQM_3, SETFAM_1, XBOOLE_0, XBOOLE_1, XXREAL_0, ORDINAL1, PARTFUN1, PRE_POLY, NUMBERS;
schemes PBOOLE, CLASSES1, MSSUBFAM, PRE_POLY;
registrations XBOOLE_0, SETFAM_1, RELAT_1, FINSET_1, FINSUB_1, XXREAL_0, NAT_1, FINSEQ_1, STRUCT_0, ORDERS_2, MEMBERED, VALUED_0, CARD_1, RELSET_1, FUNCT_1, FUNCT_2, PRE_POLY, ORDINAL1, XCMPLX_0;
constructors HIDDEN, SETFAM_1, DOMAIN_1, FINSEQOP, PBOOLE, ORDERS_2, RELSET_1, PRE_POLY, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities WELLORD1, ORDERS_2, FINSEQ_2, SUBSET_1;
expansions RELAT_2, TARSKI, XBOOLE_0, PBOOLE;
definition
let C be non
empty Poset;
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 ) )
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
end;