environ
vocabularies HIDDEN, NUMBERS, NAT_1, SETFAM_1, TREES_2, TARSKI, CARD_1, XBOOLE_0, FINSET_1, PEPIN, XXREAL_0, ORDINAL1, ARYTM_3, ARYTM_1, SUBSET_1, FUNCT_1, RELAT_1, INT_1, PCOMPS_1, PRE_TOPC, TOPDIM_1, WAYBEL23, RCOMP_1, PROB_1, TOPGEN_4, CARD_3, ZFMISC_1, STRUCT_0, RLVECT_3, TOPS_1, MCART_1, METRIZTS, EUCLID, REAL_1, FINSEQ_1, METRIC_1, FINSEQ_2, RVSUM_1, SQUARE_1, COMPLEX1, CONNSP_1, T_0TOPSP, FUNCOP_1, FUNCT_4, CARD_2, CONVEX1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, MCART_1, ZFMISC_1, FUNCT_2, BINOP_1, CARD_1, CANTOR_1, COMPLEX1, FINSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, REAL_1, XXREAL_3, INT_1, NAT_1, SETFAM_1, DOMAIN_1, FUNCOP_1, TOPS_2, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, CARD_3, PROB_1, CONVEX1, KURATO_2, WAYBEL23, TOPS_1, T_0TOPSP, CARD_2, RVSUM_1, FINSEQ_1, FINSEQ_2, EUCLID, BORSUK_1, TOPGEN_4, FUNCT_4, SQUARE_1, CONNSP_1, TOPREAL9, ORDERS_4, METRIZTS, TOPDIM_1;
definitions TARSKI, XBOOLE_0, TOPS_2, SETFAM_1;
theorems ABSVALUE, FINSEQ_1, FINSEQ_2, FUNCT_1, FUNCT_2, RVSUM_1, TARSKI, XREAL_0, COMPLEX1, XREAL_1, XXREAL_0, FUNCOP_1, ORDINAL1, RELAT_1, PRE_TOPC, TOPMETR, EUCLID, METRIC_1, XBOOLE_0, TOPS_1, TOPS_2, TOPREAL7, PROB_1, ZFMISC_1, NAT_1, KURATO_2, INT_1, TOPGEN_1, XBOOLE_1, MCART_1, CARD_1, TOPGEN_4, SUBSET_1, TSEP_1, TSP_1, SETFAM_1, CARD_4, YELLOW_9, ORDERS_4, BORSUK_1, CARD_3, CARD_2, NECKLACE, BORSUK_3, TOPALG_3, TOPREAL9, JORDAN2B, JORDAN, STIRL2_1, FUNCT_4, ENUMSET1, XXREAL_3, CONNSP_1, WELLORD2, METRIZTS, PCOMPS_1, TOPDIM_1, YELLOW14, XTUPLE_0;
schemes FUNCT_2, NAT_1, CLASSES1, LMOD_7, BORSUK_2;
registrations PRE_TOPC, PCOMPS_1, NAT_1, XREAL_0, SUBSET_1, STRUCT_0, TOPS_1, XXREAL_0, YELLOW13, CARD_1, XBOOLE_0, FINSET_1, VALUED_0, RELAT_1, FUNCT_1, INT_1, CARD_3, TOPGEN_4, BORSUK_3, BORSUK_1, XXREAL_3, METRIZTS, TOPDIM_1, EUCLID, RELSET_1, JORDAN1, JORDAN2C, XTUPLE_0, ORDINAL1;
constructors HIDDEN, TOPS_2, BORSUK_1, REAL_1, COMPLEX1, CANTOR_1, TOPGEN_4, WAYBEL23, TOPS_1, SQUARE_1, RVSUM_1, BORSUK_3, CARD_2, CONNSP_1, BINOP_2, TOPREAL9, ORDERS_4, XXREAL_3, METRIZTS, TOPDIM_1, FUNCSDOM, PCOMPS_1, CONVEX1, XTUPLE_0, NUMBERS;
requirements HIDDEN, REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
equalities STRUCT_0, SQUARE_1, EUCLID, PCOMPS_1, TOPS_1, METRIC_1, SUBSET_1, CARD_3, TOPDIM_1, CARD_1, ORDINAL1;
expansions PCOMPS_1, TARSKI, XBOOLE_0, TOPS_2, CARD_3, TOPDIM_1;
Lm1:
for T being TopSpace
for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat
Lm2:
for n being Nat
for T being TopSpace
for g being SetSequence of T st ( for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) holds
ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G )
Lm3:
for n being Nat
for T being metrizable TopSpace st T is second-countable holds
( ( ex F being Subset-Family of T st
( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st
( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) )
Lm4:
for TM being metrizable TopSpace
for A, B being Subset of TM st A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable holds
( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 )
Lm5:
for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) holds
( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
Lm6:
TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1)
by EUCLID:def 8;
Lm7:
( TOP-REAL 0 is finite-ind & ind (TOP-REAL 0) = 0 )
Lm8:
( TOP-REAL 1 is finite-ind & ind (TOP-REAL 1) = 1 )
Lm9:
for n being Nat holds
( TOP-REAL n is finite-ind & ind (TOP-REAL n) <= n )
Lm10:
for TM being metrizable TopSpace
for A being finite-ind Subset of TM st TM | A is second-countable & ind (TM | A) <= 0 holds
for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds
ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 )