environ
vocabularies HIDDEN, NUMBERS, PRE_TOPC, SUBSET_1, RELAT_1, SETFAM_1, RCOMP_1, NAT_1, INT_1, XBOOLE_0, TOPS_1, TARSKI, PROB_1, ZFMISC_1, STRUCT_0, FUNCT_1, CARD_1, ARYTM_3, PARTFUN1, FINSET_1, XXREAL_0, COMPTS_1, ARYTM_1, ORDINAL1, T_0TOPSP, TOPS_2, CARD_5, METRIZTS, RLVECT_3, CARD_3, MCART_1, PCOMPS_1, WAYBEL23, TOPDIM_1, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, ORDINAL1, XTUPLE_0, MCART_1, FUNCT_2, CARD_1, CARD_3, CANTOR_1, FINSET_1, NUMBERS, ZFMISC_1, XXREAL_0, XCMPLX_0, REAL_1, SETFAM_1, DOMAIN_1, PRE_TOPC, TOPS_1, TOPS_2, INT_1, NAT_1, STRUCT_0, COMPTS_1, PCOMPS_1, PROB_1, WAYBEL23, BORSUK_1, BORSUK_3, METRIZTS;
definitions TOPS_2, TARSKI, XBOOLE_0;
theorems CARD_2, CARD_3, FUNCT_1, FUNCT_2, INT_1, ORDINAL1, MCART_1, NAT_1, PRE_TOPC, PROB_1, RELAT_1, SETFAM_1, SETLIM_1, SUBSET_1, TARSKI, TOPGEN_1, TOPGRP_1, TOPS_1, TOPS_2, TOPS_3, TSEP_1, TSP_1, T_0TOPSP, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, YELLOW12, YELLOW_9, ZFMISC_1, METRIZTS, KURATO_0, XTUPLE_0;
schemes CLASSES1, FRAENKEL, FUNCT_2, NAT_1, SUBSET_1;
registrations BORSUK_3, CARD_1, COMPTS_1, FINSET_1, FUNCT_2, INT_1, NAT_1, ORDINAL1, PRE_TOPC, STRUCT_0, SUBSET_1, TOPREAL6, TOPS_1, XCMPLX_0, XREAL_0, XXREAL_0, YELLOW13, METRIZTS, RELSET_1, BORSUK_1, XTUPLE_0;
constructors HIDDEN, TOPS_1, TOPS_2, BORSUK_1, REAL_1, CANTOR_1, WAYBEL23, COMPTS_1, BORSUK_3, METRIZTS, PCOMPS_1, KURATO_0, EUCLID, XTUPLE_0;
requirements HIDDEN, ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
equalities COMPTS_1, STRUCT_0, SUBSET_1, TOPS_1, XBOOLE_0, CARD_1, ORDINAL1;
expansions TOPS_2, TARSKI, XBOOLE_0, FUNCT_2;
Lm1:
for T being TopSpace
for A being finite Subset of T holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) )
Lm2:
for X being set holds X in (Seq_of_ind (1TopSp X)) . 1
Lm3:
for T being TopSpace
for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat
Lm4:
for T being TopSpace
for G, G1 being Subset-Family of T
for i being Integer st G is finite-ind & G1 is finite-ind & ind G <= i & ind G1 <= i holds
( G \/ G1 is finite-ind & ind (G \/ G1) <= i )
Lm5:
for T being TopSpace
for Af being finite-ind Subset of T holds
( T | Af is finite-ind & ind (T | Af) = ind Af )
Lm6:
for Tf being finite-ind TopSpace
for A being Subset of Tf holds
( Tf | A is finite-ind & ind (Tf | A) <= ind Tf )
Lm7:
for T being TopSpace
for A being Subset of T st T is finite-ind holds
A is finite-ind
Lm8:
for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind holds
( T2 is finite-ind & ind T2 <= ind T1 )
Lm9:
for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds
( ( T1 is finite-ind implies T2 is finite-ind ) & ( T2 is finite-ind implies T1 is finite-ind ) & ( T1 is finite-ind implies ind T2 = ind T1 ) )
:: with limited small inductive dimension