:: Small {I}nductive {D}imension of {T}opological {S}paces
:: by Karol P\c{a}k
::
:: Received June 29, 2009
:: Copyright (c) 2009 Association of Mizar Users
theorem Th1: :: TOPDIM_1:1
theorem Th2: :: TOPDIM_1:2
:: deftheorem Def1 defines Seq_of_ind TOPDIM_1:def 1 :
theorem Th3: :: TOPDIM_1:3
:: 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: :: TOPDIM_1:4
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
:: deftheorem Def5 defines ind TOPDIM_1:def 5 :
theorem Th5: :: TOPDIM_1:5
theorem Th6: :: TOPDIM_1:6
Lm3:
for T being TopSpace
for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat
theorem Th7: :: TOPDIM_1:7
theorem :: TOPDIM_1:8
theorem Th9: :: TOPDIM_1:9
:: deftheorem Def6 defines ind TOPDIM_1:def 6 :
theorem :: TOPDIM_1:10
theorem Th11: :: TOPDIM_1:11
theorem :: TOPDIM_1:12
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 :: TOPDIM_1:13
:: deftheorem defines ind TOPDIM_1:def 7 :
theorem :: TOPDIM_1:14
theorem Th15: :: TOPDIM_1:15
theorem Th16: :: TOPDIM_1:16
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
theorem :: TOPDIM_1:17
theorem Th18: :: TOPDIM_1:18
theorem Th19: :: TOPDIM_1:19
theorem :: TOPDIM_1:20
theorem Th21: :: TOPDIM_1:21
theorem Th22: :: TOPDIM_1:22
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 :: TOPDIM_1:23
theorem :: TOPDIM_1:24
theorem :: TOPDIM_1:25
theorem Th26: :: TOPDIM_1:26
theorem :: TOPDIM_1:27
theorem :: TOPDIM_1:28
theorem :: TOPDIM_1:29
theorem :: TOPDIM_1:30
theorem Th31: :: TOPDIM_1:31
theorem Th32: :: TOPDIM_1:32
theorem Th33: :: TOPDIM_1:33
theorem Th34: :: TOPDIM_1:34
theorem Th35: :: TOPDIM_1:35
theorem :: TOPDIM_1:36
theorem Th37: :: TOPDIM_1:37
theorem Th38: :: TOPDIM_1:38
theorem Th39: :: TOPDIM_1:39
theorem :: TOPDIM_1:40