begin
theorem Th1:
theorem Th2:
:: deftheorem Def1 defines Seq_of_ind TOPDIM_1:def 1 :
theorem Th3:
:: deftheorem Def2 defines with_finite_small_inductive_dimension TOPDIM_1:def 2 :
:: deftheorem Def3 defines with_finite_small_inductive_dimension TOPDIM_1:def 3 :
theorem Th4:
Lm1:
for T being TopSpace
for A being finite Subset of T holds
( A is with_finite_small_inductive_dimension & A in (Seq_of_ind T) . (card A) )
:: deftheorem Def4 defines with_finite_small_inductive_dimension TOPDIM_1:def 4 :
Lm2:
for X being set holds X in (Seq_of_ind (1TopSp X)) . 1
begin
:: deftheorem Def5 defines ind TOPDIM_1:def 5 :
theorem Th5:
theorem Th6:
Lm3:
for T being TopSpace
for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat
theorem Th7:
theorem
theorem Th9:
:: deftheorem Def6 defines ind TOPDIM_1:def 6 :
theorem
theorem Th11:
theorem
Lm4:
for T being TopSpace
for G, G1 being Subset-Family of T
for i being Integer st G is with_finite_small_inductive_dimension & G1 is with_finite_small_inductive_dimension & ind G <= i & ind G1 <= i holds
( G \/ G1 is with_finite_small_inductive_dimension & ind (G \/ G1) <= i )
theorem
:: deftheorem defines ind TOPDIM_1:def 7 :
theorem
theorem Th15:
theorem Th16:
Lm5:
for T being TopSpace
for Af being finite-ind Subset of T holds
( T | Af is with_finite_small_inductive_dimension & ind (T | Af) = ind Af )
Lm6:
for Tf being finite-ind TopSpace
for A being Subset of Tf holds
( Tf | A is with_finite_small_inductive_dimension & ind (Tf | A) <= ind Tf )
Lm7:
for T being TopSpace
for A being Subset of T st T is with_finite_small_inductive_dimension holds
A is with_finite_small_inductive_dimension
begin
theorem
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
Lm8:
for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is with_finite_small_inductive_dimension holds
( T2 is with_finite_small_inductive_dimension & ind T2 <= ind T1 )
Lm9:
for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds
( ( T1 is with_finite_small_inductive_dimension implies T2 is with_finite_small_inductive_dimension ) & ( T2 is with_finite_small_inductive_dimension implies T1 is with_finite_small_inductive_dimension ) & ( T1 is with_finite_small_inductive_dimension implies ind T2 = ind T1 ) )
theorem
theorem
theorem
theorem Th26:
theorem
theorem
theorem
theorem
begin
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem Th38:
theorem Th39:
theorem