environ
vocabularies HIDDEN, ARYTM_1, XBOOLE_0, CARD_1, CLASSES1, COHSP_1, FINSET_1, FUNCT_1, GROUP_4, INT_1, MATROID0, ORDERS_1, PARTFUN1, PRE_TOPC, RELAT_1, RELAT_2, NUMBERS, SETFAM_1, SGRAPH1, SUBSET_1, TARSKI, TRIANG_1, WELLORD1, ZFMISC_1, SIMPLEX0, XXREAL_0, NAT_1, ORDINAL1, FUNCOP_1, ARYTM_3, RCOMP_1, STRUCT_0, GLIB_000, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, RELAT_2, FUNCT_1, FUNCT_2, ORDINAL1, NUMBERS, WELLORD1, ORDERS_1, FINSET_1, CARD_1, XCMPLX_0, XREAL_0, XXREAL_0, INT_1, XXREAL_3, NAT_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, PENCIL_1, CLASSES1, MATROID0, RELSET_1, COHSP_1, FUNCOP_1;
definitions CLASSES1, FINSET_1, MATROID0, ORDINAL1, SETFAM_1, TARSKI, TOPS_2, XBOOLE_0;
theorems CARD_1, CARD_2, CLASSES1, COHSP_1, COMBGRAS, FINSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, INT_1, MATROID0, NAT_1, ORDERS_1, ORDINAL1, PENCIL_1, PRE_TOPC, RELAT_1, RELAT_2, SETFAM_1, STIRL2_1, SUBSET_1, WELLORD1, WELLORD2, TARSKI, TOPS_2, XREAL_0, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, XXREAL_3, ZFMISC_1;
schemes CLASSES1, FRAENKEL, FUNCT_2, NAT_1;
registrations PRE_TOPC, CARD_1, COHSP_1, FIB_NUM2, FINSET_1, FUNCT_1, INT_1, MATROID0, NAT_1, ORDINAL1, PENCIL_1, RELAT_1, SETFAM_1, SUBSET_1, STRUCT_0, XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_3, FUNCOP_1, RELSET_1;
constructors HIDDEN, SETFAM_1, XXREAL_3, REAL_1, TOPS_2, BORSUK_1, WELLORD1, BINOP_2, CLASSES1, COH_SP, MATROID0, COHSP_1, FUNCOP_1, NAT_1;
requirements HIDDEN, REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
equalities MATROID0, ORDINAL1, STRUCT_0, SUBSET_1, TARSKI, XXREAL_3, CARD_1;
expansions CLASSES1, FINSET_1, MATROID0, ORDINAL1, SETFAM_1, TARSKI, TOPS_2, XBOOLE_0;
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 ) )
Lm2:
for K being SimplicialComplexStr holds
( Vertices K is empty iff K is empty-membered )
Lm3:
for x being set
for K being SimplicialComplexStr
for S being Subset of K st S is simplex-like & x in S holds
x in Vertices K
Lm4:
for K being SimplicialComplexStr
for A being Subset of K st A is simplex-like holds
A c= Vertices K
by Lm3;
Lm5:
for K being SimplicialComplexStr holds Vertices K = union the topology of K
Lm6:
for K being SimplicialComplexStr st K is finite-vertices holds
the topology of K is finite
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