TOPDIM_1: Small {I}nductive {D}imension of {T}opological {S}paces

:: 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Seq_of_ind TOPDIM_1:def 1 :

registration

let T be TopSpace;
cluster Seq_of_ind T -> non-descending ;
coherence

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 :

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 :

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 by Lm1;
cluster empty -> finite-ind Element of bool (bool the carrier of T);
coherence

proof end;

cluster non empty finite-ind Element of bool (bool the carrier of T);
existence

proof end;

end;

registration

let T be non empty TopSpace;
cluster non empty finite-ind Element of bool the carrier of T;
existence

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 :

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

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

proof end;

end;

registration

cluster non empty TopSpace-like finite-ind TopStruct ;
existence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ind TOPDIM_1:def 5 :

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines ind TOPDIM_1:def 6 :

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

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 ;

end;

:: deftheorem defines ind TOPDIM_1:def 7 :

registration

let T be non empty finite-ind TopSpace;
cluster ind T -> natural ;
coherence

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 by Lm7;

end;

registration

let T be TopSpace;
let Af be finite-ind Subset of T;
cluster T | Af -> finite-ind ;
coherence 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;