begin
:: deftheorem Def1 defines finite-order TOPDIM_2:def 1 :
for X being set
for Fx being Subset-Family of X holds
( Fx is finite-order iff ex n being Nat st
for Gx being Subset-Family of X st Gx c= Fx & n in card Gx holds
meet Gx is empty );
:: deftheorem Def2 defines order TOPDIM_2:def 2 :
for X being set
for Fx being Subset-Family of X
for b3 being ext-real number holds
( ( Fx is finite-order implies ( b3 = order Fx iff ( ( for Gx being Subset-Family of X st b3 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b3 + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) ) & ( not Fx is finite-order implies ( b3 = order Fx iff b3 = +infty ) ) );
theorem Th1:
theorem
theorem Th3:
begin
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 with_finite_small_inductive_dimension & ind (g . i) <= n & g . i is F_sigma ) ) holds
ex G being Subset-Family of T st
( G is closed & G is with_finite_small_inductive_dimension & 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 with_finite_small_inductive_dimension & ind F <= n ) implies ( T is with_finite_small_inductive_dimension & ind T <= n ) ) & ( T is with_finite_small_inductive_dimension & 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 ) ) )
theorem
theorem Th5:
theorem
theorem Th7:
theorem Th8:
Lm4:
for TM being metrizable TopSpace
for A, B being Subset of TM st A is with_finite_small_inductive_dimension & B is with_finite_small_inductive_dimension & TM | (A \/ B) is second-countable holds
( A \/ B is with_finite_small_inductive_dimension & ind (A \/ B) <= ((ind A) + (ind B)) + 1 )
theorem
theorem Th10:
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 with_finite_small_inductive_dimension & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
theorem Th11:
theorem
theorem Th13:
theorem
theorem
theorem
begin
theorem Th17:
A:
TopStruct(# the carrier of (TOP-REAL 1),the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1)
by EUCLID:def 8;
theorem Th18:
theorem Th19:
Lm6:
( TOP-REAL 0 is with_finite_small_inductive_dimension & ind (TOP-REAL 0 ) = 0 )
Lm7:
( TOP-REAL 1 is with_finite_small_inductive_dimension & ind (TOP-REAL 1) = 1 )
Lm8:
for n being Nat holds
( TOP-REAL n is with_finite_small_inductive_dimension & ind (TOP-REAL n) <= n )
theorem
theorem
Lm9:
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 )
theorem Th22:
theorem
theorem