:: Small Inductive Dimension of Topological Spaces, Part {II}
:: by Karol P\c{a}k
::
:: Received August 7, 2009
:: Copyright (c) 2009 Association of Mizar Users
:: deftheorem Def1 defines finite-order TOPDIM_2:def 1 :
:: deftheorem Def2 defines order TOPDIM_2:def 2 :
theorem Th1: :: TOPDIM_2:1
theorem :: TOPDIM_2:2
theorem Th3: :: TOPDIM_2:3
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 :: TOPDIM_2:4
theorem Th5: :: TOPDIM_2:5
theorem :: TOPDIM_2:6
theorem Th7: :: TOPDIM_2:7
theorem Th8: :: TOPDIM_2:8
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 :: TOPDIM_2:9
theorem Th10: :: TOPDIM_2:10
Lm5:
for TM1, TM2 being metrizable second-countable finite-ind 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: :: TOPDIM_2:11
theorem :: TOPDIM_2:12
theorem Th13: :: TOPDIM_2:13
theorem :: TOPDIM_2:14
theorem :: TOPDIM_2:15
theorem :: TOPDIM_2:16
theorem Th17: :: TOPDIM_2:17
A:
TopStruct(# the carrier of (TOP-REAL 1),the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1)
by EUCLID:def 8;
theorem Th18: :: TOPDIM_2:18
theorem Th19: :: TOPDIM_2:19
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 :: TOPDIM_2:20
theorem :: TOPDIM_2:21
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: :: TOPDIM_2:22
theorem :: TOPDIM_2:23
theorem :: TOPDIM_2:24