:: Small {I}nductive {D}imension of {T}opological {S}paces
:: by Karol P\c{a}k
::
:: Received June 29, 2009
:: Copyright (c) 2009-2011 Association of Mizar Users


begin

theorem Th1: :: TOPDIM_1:1
for T being TopSpace
for B, A being Subset of T
for F being Subset of (T | A) st F = B /\ A holds
Fr F c= (Fr B) /\ A
proof end;

theorem Th2: :: TOPDIM_1:2
for T being TopSpace holds
( T is normal iff for A, B being closed Subset of T st A misses B holds
ex U, W being open Subset of T st
( A c= U & B c= W & Cl U misses Cl W ) )
proof end;

definition
let T be TopSpace;
func Seq_of_ind T -> SetSequence of (bool the carrier of T) means :Def1: :: TOPDIM_1:def 1
for A being Subset of T
for n being Nat holds
( it . 0 = {({} T)} & ( not A in it . (n + 1) or A in it . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in it . n ) ) & ( ( A in it . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in it . n ) ) implies A in it . (n + 1) ) );
existence
ex b1 being SetSequence of (bool the carrier of T) st
for A being Subset of T
for n being Nat holds
( b1 . 0 = {({} T)} & ( not A in b1 . (n + 1) or A in b1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b1 . n ) ) & ( ( A in b1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b1 . n ) ) implies A in b1 . (n + 1) ) )
proof end;
uniqueness
for b1, b2 being SetSequence of (bool the carrier of T) st ( for A being Subset of T
for n being Nat holds
( b1 . 0 = {({} T)} & ( not A in b1 . (n + 1) or A in b1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b1 . n ) ) & ( ( A in b1 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b1 . n ) ) implies A in b1 . (n + 1) ) ) ) & ( for A being Subset of T
for n being Nat holds
( b2 . 0 = {({} T)} & ( not A in b2 . (n + 1) or A in b2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b2 . n ) ) & ( ( A in b2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b2 . n ) ) implies A in b2 . (n + 1) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Seq_of_ind TOPDIM_1:def 1 :
for T being TopSpace
for b2 being SetSequence of (bool the carrier of T) holds
( b2 = Seq_of_ind T iff for A being Subset of T
for n being Nat holds
( b2 . 0 = {({} T)} & ( not A in b2 . (n + 1) or A in b2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b2 . n ) ) & ( ( A in b2 . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in b2 . n ) ) implies A in b2 . (n + 1) ) ) );

registration
let T be TopSpace;
cluster Seq_of_ind T -> non-descending ;
coherence
Seq_of_ind T is non-descending
proof end;
end;

theorem Th3: :: TOPDIM_1:3
for T being TopSpace
for A, B being Subset of T
for n being Nat
for F being Subset of (T | A) st F = B holds
( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n )
proof end;

definition
let T be TopSpace;
let A be Subset of T;
attr A is with_finite_small_inductive_dimension means :Def2: :: TOPDIM_1:def 2
ex n being Nat st A in (Seq_of_ind T) . n;
end;

:: deftheorem Def2 defines with_finite_small_inductive_dimension TOPDIM_1:def 2 :
for T being TopSpace
for A being Subset of T holds
( A is with_finite_small_inductive_dimension iff ex n being Nat st A in (Seq_of_ind T) . n );

notation
let T be TopSpace;
let A be Subset of T;
synonym finite-ind A for with_finite_small_inductive_dimension ;
end;

definition
let T be TopSpace;
let G be Subset-Family of T;
attr G is with_finite_small_inductive_dimension means :Def3: :: TOPDIM_1:def 3
ex n being Nat st G c= (Seq_of_ind T) . n;
end;

:: deftheorem Def3 defines with_finite_small_inductive_dimension TOPDIM_1:def 3 :
for T being TopSpace
for G being Subset-Family of T holds
( G is with_finite_small_inductive_dimension iff ex n being Nat st G c= (Seq_of_ind T) . n );

notation
let T be TopSpace;
let G be Subset-Family of T;
synonym finite-ind G for with_finite_small_inductive_dimension ;
end;

theorem Th4: :: TOPDIM_1:4
for T being TopSpace
for A being Subset of T
for G being Subset-Family of T st A in G & G is with_finite_small_inductive_dimension holds
A is with_finite_small_inductive_dimension
proof end;

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) )
proof end;

registration
let T be TopSpace;
cluster finite -> finite-ind Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is finite holds
b1 is with_finite_small_inductive_dimension
by Lm1;
cluster empty -> finite-ind Element of bool (bool the carrier of T);
coherence
for b1 being Subset-Family of T st b1 is empty holds
b1 is with_finite_small_inductive_dimension
proof end;
cluster non empty finite-ind Element of bool (bool the carrier of T);
existence
ex b1 being Subset-Family of T st
( not b1 is empty & b1 is with_finite_small_inductive_dimension )
proof end;
end;

registration
let T be non empty TopSpace;
cluster non empty finite-ind Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( not b1 is empty & b1 is with_finite_small_inductive_dimension )
proof end;
end;

definition
let T be TopSpace;
attr T is with_finite_small_inductive_dimension means :Def4: :: TOPDIM_1:def 4
[#] T is with_finite_small_inductive_dimension ;
end;

:: deftheorem Def4 defines with_finite_small_inductive_dimension TOPDIM_1:def 4 :
for T being TopSpace holds
( T is with_finite_small_inductive_dimension iff [#] T is with_finite_small_inductive_dimension );

notation
let T be TopSpace;
synonym finite-ind T for with_finite_small_inductive_dimension ;
end;

registration
cluster empty TopSpace-like -> finite-ind TopStruct ;
coherence
for b1 being TopSpace st b1 is empty holds
b1 is with_finite_small_inductive_dimension
proof end;
end;

Lm2: for X being set holds X in (Seq_of_ind (1TopSp X)) . 1
proof end;

registration
let X be set ;
cluster 1TopSp X -> finite-ind ;
coherence
1TopSp X is with_finite_small_inductive_dimension
proof end;
end;

registration
cluster non empty TopSpace-like finite-ind TopStruct ;
existence
ex b1 being TopSpace st
( not b1 is empty & b1 is with_finite_small_inductive_dimension )
proof end;
end;

begin

definition
let T be TopSpace;
let A be Subset of T;
assume A1: A is with_finite_small_inductive_dimension ;
func ind A -> Integer means :Def5: :: TOPDIM_1:def 5
( A in (Seq_of_ind T) . (it + 1) & not A in (Seq_of_ind T) . it );
existence
ex b1 being Integer st
( A in (Seq_of_ind T) . (b1 + 1) & not A in (Seq_of_ind T) . b1 )
proof end;
uniqueness
for b1, b2 being Integer st A in (Seq_of_ind T) . (b1 + 1) & not A in (Seq_of_ind T) . b1 & A in (Seq_of_ind T) . (b2 + 1) & not A in (Seq_of_ind T) . b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines ind TOPDIM_1:def 5 :
for T being TopSpace
for A being Subset of T st A is with_finite_small_inductive_dimension holds
for b3 being Integer holds
( b3 = ind A iff ( A in (Seq_of_ind T) . (b3 + 1) & not A in (Seq_of_ind T) . b3 ) );

theorem Th5: :: TOPDIM_1:5
for T being TopSpace
for Af being finite-ind Subset of T holds - 1 <= ind Af
proof end;

theorem Th6: :: TOPDIM_1:6
for T being TopSpace
for Af being finite-ind Subset of T holds
( ind Af = - 1 iff Af is empty )
proof end;

Lm3: for T being TopSpace
for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat
proof end;

registration
let T be non empty TopSpace;
let A be non empty finite-ind Subset of T;
cluster ind A -> natural ;
coherence
ind A is natural
proof end;
end;

theorem Th7: :: TOPDIM_1:7
for T being TopSpace
for n being Nat
for Af being finite-ind Subset of T holds
( ind Af <= n - 1 iff Af in (Seq_of_ind T) . n )
proof end;

theorem :: TOPDIM_1:8
for T being TopSpace
for A being finite Subset of T holds ind A < card A
proof end;

theorem Th9: :: TOPDIM_1:9
for T being TopSpace
for n being Nat
for Af being finite-ind Subset of T holds
( ind Af <= n iff for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= n - 1 ) )
proof end;

definition
let T be TopSpace;
let G be Subset-Family of T;
assume A1: G is with_finite_small_inductive_dimension ;
func ind G -> Integer means :Def6: :: TOPDIM_1:def 6
( G c= (Seq_of_ind T) . (it + 1) & - 1 <= it & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
it <= i ) );
existence
ex b1 being Integer st
( G c= (Seq_of_ind T) . (b1 + 1) & - 1 <= b1 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b1 <= i ) )
proof end;
uniqueness
for b1, b2 being Integer st G c= (Seq_of_ind T) . (b1 + 1) & - 1 <= b1 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b1 <= i ) & G c= (Seq_of_ind T) . (b2 + 1) & - 1 <= b2 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b2 <= i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines ind TOPDIM_1:def 6 :
for T being TopSpace
for G being Subset-Family of T st G is with_finite_small_inductive_dimension holds
for b3 being Integer holds
( b3 = ind G iff ( G c= (Seq_of_ind T) . (b3 + 1) & - 1 <= b3 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b3 <= i ) ) );

theorem :: TOPDIM_1:10
for T being TopSpace
for G being Subset-Family of T holds
( ( ind G = - 1 & G is with_finite_small_inductive_dimension ) iff G c= {({} T)} )
proof end;

theorem Th11: :: TOPDIM_1:11
for T being TopSpace
for G being Subset-Family of T
for I being Integer holds
( G is with_finite_small_inductive_dimension & ind G <= I iff ( - 1 <= I & ( for A being Subset of T st A in G holds
( A is with_finite_small_inductive_dimension & ind A <= I ) ) ) )
proof end;

theorem :: TOPDIM_1:12
for T being TopSpace
for G1, G2 being Subset-Family of T st G1 is with_finite_small_inductive_dimension & G2 c= G1 holds
( G2 is with_finite_small_inductive_dimension & ind G2 <= ind G1 )
proof end;

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 )
proof end;

registration
let T be TopSpace;
let G1, G2 be finite-ind Subset-Family of T;
cluster G1 \/ G2 -> finite-ind Subset-Family of T;
coherence
for b1 being Subset-Family of T st b1 = G1 \/ G2 holds
b1 is with_finite_small_inductive_dimension
proof end;
end;

theorem :: TOPDIM_1:13
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
ind (G \/ G1) <= I by Lm4;

definition
let T be TopSpace;
func ind T -> Integer equals :: TOPDIM_1:def 7
ind ([#] T);
correctness
coherence
ind ([#] T) is Integer
;
;
end;

:: deftheorem defines ind TOPDIM_1:def 7 :
for T being TopSpace holds ind T = ind ([#] T);

registration
let T be non empty finite-ind TopSpace;
cluster ind T -> natural ;
coherence
ind T is natural
proof end;
end;

theorem :: TOPDIM_1:14
for X being non empty set holds ind (1TopSp X) = 0
proof end;

theorem Th15: :: TOPDIM_1:15
for T being TopSpace st ex n being Nat st
for p being Point of T
for U being open Subset of T st p in U holds
ex W being open Subset of T st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= n - 1 ) holds
T is with_finite_small_inductive_dimension
proof end;

theorem Th16: :: TOPDIM_1:16
for n being Nat
for Tf being finite-ind TopSpace holds
( ind Tf <= n iff for p being Point of Tf
for U being open Subset of Tf st p in U holds
ex W being open Subset of Tf st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= n - 1 ) )
proof end;

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 )
proof end;

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 )
proof end;

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
proof end;

begin

registration
let Tf be finite-ind TopSpace;
cluster -> finite-ind Element of bool the carrier of Tf;
coherence
for b1 being Subset of Tf holds b1 is with_finite_small_inductive_dimension
by Lm7;
end;

registration
let T be TopSpace;
let Af be finite-ind Subset of T;
cluster T | Af -> finite-ind ;
coherence
T | Af is with_finite_small_inductive_dimension
by Lm5;
end;

theorem :: TOPDIM_1:17
for T being TopSpace
for Af being finite-ind Subset of T holds ind (T | Af) = ind Af by Lm5;

theorem Th18: :: TOPDIM_1:18
for T being TopSpace
for A being Subset of T st T | A is with_finite_small_inductive_dimension holds
A is with_finite_small_inductive_dimension
proof end;

theorem Th19: :: TOPDIM_1:19
for T being TopSpace
for A being Subset of T
for Af being finite-ind Subset of T st A c= Af holds
( A is with_finite_small_inductive_dimension & ind A <= ind Af )
proof end;

theorem :: TOPDIM_1:20
for Tf being finite-ind TopSpace
for A being Subset of Tf holds ind A <= ind Tf by Th19;

theorem Th21: :: TOPDIM_1:21
for T being TopSpace
for A, B being Subset of T
for F being Subset of (T | A) st F = B & B is with_finite_small_inductive_dimension holds
( F is with_finite_small_inductive_dimension & ind F = ind B )
proof end;

theorem Th22: :: TOPDIM_1:22
for T being TopSpace
for A, B being Subset of T
for F being Subset of (T | A) st F = B & F is with_finite_small_inductive_dimension holds
( B is with_finite_small_inductive_dimension & ind F = ind B )
proof end;

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 )
proof end;

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 ) )
proof end;

theorem :: TOPDIM_1:23
for n being Nat
for T being non empty TopSpace st T is regular holds
( ( T is with_finite_small_inductive_dimension & ind T <= n ) iff for A being closed Subset of T
for p being Point of T st not p in A holds
ex L being Subset of T st
( L separates {p},A & L is with_finite_small_inductive_dimension & ind L <= n - 1 ) )
proof end;

theorem :: TOPDIM_1:24
for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds
( T1 is with_finite_small_inductive_dimension iff T2 is with_finite_small_inductive_dimension ) by Lm9;

theorem :: TOPDIM_1:25
for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is with_finite_small_inductive_dimension holds
ind T1 = ind T2 by Lm9;

theorem Th26: :: TOPDIM_1:26
for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is with_finite_small_inductive_dimension iff A2 is with_finite_small_inductive_dimension )
proof end;

theorem :: TOPDIM_1:27
for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic & A1 is with_finite_small_inductive_dimension holds
ind A1 = ind A2
proof end;

theorem :: TOPDIM_1:28
for T1, T2 being TopSpace st [:T1,T2:] is with_finite_small_inductive_dimension holds
( [:T2,T1:] is with_finite_small_inductive_dimension & ind [:T1,T2:] = ind [:T2,T1:] )
proof end;

theorem :: TOPDIM_1:29
for T being TopSpace
for A being Subset of T
for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st Ga is with_finite_small_inductive_dimension & Ga = G holds
( G is with_finite_small_inductive_dimension & ind G = ind Ga )
proof end;

theorem :: TOPDIM_1:30
for T being TopSpace
for A being Subset of T
for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st G is with_finite_small_inductive_dimension & Ga = G holds
( Ga is with_finite_small_inductive_dimension & ind G = ind Ga )
proof end;

begin

theorem Th31: :: TOPDIM_1:31
for T being TopSpace
for n being Nat holds
( ( T is with_finite_small_inductive_dimension & ind T <= n ) iff ex Bas being Basis of T st
for A being Subset of T st A in Bas holds
( Fr A is with_finite_small_inductive_dimension & ind (Fr A) <= n - 1 ) )
proof end;

theorem Th32: :: TOPDIM_1:32
for T being TopSpace st T is T_1 & ( for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) ) holds
( T is with_finite_small_inductive_dimension & ind T <= 0 )
proof end;

theorem Th33: :: TOPDIM_1:33
for X being set
for f being SetSequence of X ex g being SetSequence of X st
( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) ) )
proof end;

theorem Th34: :: TOPDIM_1:34
for T being TopSpace st T is with_finite_small_inductive_dimension & ind T <= 0 & T is Lindelof holds
for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
proof end;

theorem Th35: :: TOPDIM_1:35
for T being TopSpace st T is T_1 & T is Lindelof holds
( ( T is with_finite_small_inductive_dimension & ind T <= 0 ) iff for A, B being closed Subset of T st A misses B holds
{} T separates A,B )
proof end;

theorem :: TOPDIM_1:36
for T being TopSpace st T is T_4 & T is Lindelof & 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 <= 0 ) holds
( T is with_finite_small_inductive_dimension & ind T <= 0 )
proof end;

theorem Th37: :: TOPDIM_1:37
for TM being metrizable TopSpace
for A, B being closed Subset of TM st A misses B holds
for Null being finite-ind Subset of TM st ind Null <= 0 & TM | Null is second-countable holds
ex L being Subset of TM st
( L separates A,B & L misses Null )
proof end;

theorem Th38: :: TOPDIM_1:38
for TM being metrizable TopSpace
for Null being Subset of TM st TM | Null is second-countable holds
( ( Null is with_finite_small_inductive_dimension & ind Null <= 0 ) iff for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & Null misses Fr W ) )
proof end;

theorem Th39: :: TOPDIM_1:39
for TM being metrizable TopSpace
for Null being Subset of TM st TM | Null is second-countable holds
( ( Null is with_finite_small_inductive_dimension & ind Null <= 0 ) iff ex B being Basis of TM st
for A being Subset of TM st A in B holds
Null misses Fr A )
proof end;

theorem :: TOPDIM_1:40
for TM being metrizable TopSpace
for Null, A being Subset of TM st TM | Null is second-countable & Null is with_finite_small_inductive_dimension & A is with_finite_small_inductive_dimension & ind Null <= 0 holds
( A \/ Null is with_finite_small_inductive_dimension & ind (A \/ Null) <= (ind A) + 1 )
proof end;