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

theorem Th1: :: TOPDIM_1:1

for T being TopSpace
for A, B 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;

:: The sequence of a subset family of topological spaces
:: with limited small inductive dimension

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 b₁ being SetSequence of (bool the carrier of T) st
for A being Subset of T
for n being Nat holds
( b₁ . 0 = {({} T)} & ( not A in b₁ . (n + 1) or A in b₁ . 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 b₁ . n ) ) & ( ( A in b₁ . 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 b₁ . n ) ) implies A in b₁ . (n + 1) ) )

proof end;

uniqueness
for b₁, b₂ being SetSequence of (bool the carrier of T) st ( for A being Subset of T
for n being Nat holds
( b₁ . 0 = {({} T)} & ( not A in b₁ . (n + 1) or A in b₁ . 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 b₁ . n ) ) & ( ( A in b₁ . 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 b₁ . n ) ) implies A in b₁ . (n + 1) ) ) ) & ( for A being Subset of T
for n being Nat holds
( b₂ . 0 = {({} T)} & ( not A in b₂ . (n + 1) or A in b₂ . 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 b₂ . n ) ) & ( ( A in b₂ . 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 b₂ . n ) ) implies A in b₂ . (n + 1) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Seq_of_ind TOPDIM_1:def 1 :
for T being TopSpace
for b₂ being SetSequence of (bool the carrier of T) holds
( b₂ = Seq_of_ind T iff for A being Subset of T
for n being Nat holds
( b₂ . 0 = {({} T)} & ( not A in b₂ . (n + 1) or A in b₂ . 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 b₂ . n ) ) & ( ( A in b₂ . 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 b₂ . n ) ) implies A in b₂ . (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 :: TOPDIM_1:def 3
ex n being Nat st G c= (Seq_of_ind T) . n;

end;

:: deftheorem 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 :: 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 finite-ind holds
A is finite-ind ;

Lm1: for T being TopSpace
for A being finite Subset of T holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) )

proof end;

registration

let T be TopSpace;

cluster finite -> finite-ind for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is finite holds
b₁ is finite-ind by Lm1;

cluster empty -> finite-ind for Element of bool (bool the carrier of T);

coherence
for b₁ being Subset-Family of T st b₁ is empty holds
b₁ is finite-ind

proof end;

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

existence
ex b₁ being Subset-Family of T st
( not b₁ is empty & b₁ is finite-ind )

proof end;

end;

registration

let T be non empty TopSpace;

cluster non empty finite-ind for Element of bool the carrier of T;

existence
ex b₁ being Subset of T st
( not b₁ is empty & b₁ is finite-ind )

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 for TopStruct ;

coherence
for b₁ being TopSpace st b₁ is empty holds
b₁ is finite-ind ;

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 for TopStruct ;

existence
ex b₁ being TopSpace st
( not b₁ is empty & b₁ is finite-ind )

proof end;

end;

definition

let T be TopSpace;
let A be Subset of T;
assume A1: A is finite-ind ;

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 b₁ being Integer st
( A in (Seq_of_ind T) . (b₁ + 1) & not A in (Seq_of_ind T) . b₁ )

proof end;

uniqueness
for b₁, b₂ being Integer st A in (Seq_of_ind T) . (b₁ + 1) & not A in (Seq_of_ind T) . b₁ & A in (Seq_of_ind T) . (b₂ + 1) & not A in (Seq_of_ind T) . b₂ holds
b₁ = b₂

proof end;

end;

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

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 finite-ind & ind (Fr W) <= n - 1 ) )

proof end;

definition

let T be TopSpace;
let G be Subset-Family of T;
assume A1: G is finite-ind ;

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 b₁ being Integer st
( G c= (Seq_of_ind T) . (b₁ + 1) & - 1 <= b₁ & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b₁ <= i ) )

proof end;

uniqueness
for b₁, b₂ being Integer st G c= (Seq_of_ind T) . (b₁ + 1) & - 1 <= b₁ & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b₁ <= i ) & G c= (Seq_of_ind T) . (b₂ + 1) & - 1 <= b₂ & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b₂ <= i ) holds
b₁ = b₂

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 finite-ind holds
for b₃ being Integer holds
( b₃ = ind G iff ( G c= (Seq_of_ind T) . (b₃ + 1) & - 1 <= b₃ & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds
b₃ <= i ) ) );

theorem :: TOPDIM_1:10

for T being TopSpace
for G being Subset-Family of T holds
( ( ind G = - 1 & G is finite-ind ) 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 finite-ind & ind G <= I iff ( - 1 <= I & ( for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I ) ) ) )

proof end;

theorem :: TOPDIM_1:12

for T being TopSpace
for G1, G2 being Subset-Family of T st G1 is finite-ind & G2 c= G1 holds
( G2 is finite-ind & 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 finite-ind & G1 is finite-ind & ind G <= i & ind G1 <= i holds
( G \/ G1 is finite-ind & 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 for Subset-Family of T;

coherence
for b₁ being Subset-Family of T st b₁ = G1 \/ G2 holds
b₁ 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 finite-ind & G1 is finite-ind & 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 finite-ind & ind (Fr W) <= n - 1 ) holds
T is finite-ind

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 finite-ind & ind (Fr W) <= n - 1 ) )

proof end;

Lm5: for T being TopSpace
for Af being finite-ind Subset of T holds
( T | Af is finite-ind & ind (T | Af) = ind Af )

proof end;

Lm6: for Tf being finite-ind TopSpace
for A being Subset of Tf holds
( Tf | A is finite-ind & ind (Tf | A) <= ind Tf )

proof end;

Lm7: for T being TopSpace
for A being Subset of T st T is finite-ind holds
A is finite-ind

proof end;

registration

let Tf be finite-ind TopSpace;

cluster -> finite-ind for Element of bool the carrier of Tf;

coherence
for b₁ being Subset of Tf holds b₁ is finite-ind 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;

:: Teoria wymiaru Th 1.1.2

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 finite-ind holds
A is finite-ind

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 finite-ind & 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 finite-ind holds
( F is finite-ind & 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 finite-ind holds
( B is finite-ind & ind F = ind B )

proof end;

Lm8: for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind holds
( T2 is finite-ind & ind T2 <= ind T1 )

proof end;

Lm9: for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds
( ( T1 is finite-ind implies T2 is finite-ind ) & ( T2 is finite-ind implies T1 is finite-ind ) & ( T1 is finite-ind implies ind T2 = ind T1 ) )

proof end;

:: Teoria wymiaru Th 1.1.4

theorem :: TOPDIM_1:23

for n being Nat
for T being non empty TopSpace st T is regular holds
( ( T is finite-ind & 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 finite-ind & ind L <= n - 1 ) )

proof end;

theorem :: TOPDIM_1:24

for T1, T2 being TopSpace st T1,T2 are_homeomorphic holds
( T1 is finite-ind iff T2 is finite-ind ) by Lm9;

theorem :: TOPDIM_1:25

for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind 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 finite-ind iff A2 is finite-ind )

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 finite-ind holds
ind A1 = ind A2

proof end;

theorem :: TOPDIM_1:28

for T1, T2 being TopSpace st [:T1,T2:] is finite-ind holds
( [:T2,T1:] is finite-ind & 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 finite-ind & Ga = G holds
( G is finite-ind & 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 finite-ind & Ga = G holds
( Ga is finite-ind & ind G = ind Ga )

proof end;

:: Teoria wymiaru Th 1.1.6

theorem Th31: :: TOPDIM_1:31

for T being TopSpace
for n being Nat holds
( ( T is finite-ind & 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 finite-ind & ind (Fr A) <= n - 1 ) )

proof end;

:: Wprowadzenie do topologi 3.4.2 "=>"

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 finite-ind & 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;

:: Wprowadzenie do topologi 3.4.2 "<="

theorem Th34: :: TOPDIM_1:34

for T being TopSpace st T is finite-ind & 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;

:: Teoria wymiaru Th 1.2.6

theorem Th35: :: TOPDIM_1:35

for T being TopSpace st T is T_1 & T is Lindelof holds
( ( T is finite-ind & 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 finite-ind & ind F <= 0 ) holds
( T is finite-ind & ind T <= 0 )

proof end;

:: Teoria wymiaru Th 1.2.11

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;

:: Teoria wymiaru Th 1.2.12

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 finite-ind & 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;

:: Teoria wymiaru Th 1.2.13

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 finite-ind & 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;

:: Teoria wymiaru Th 1.5.2

theorem :: TOPDIM_1:40

for TM being metrizable TopSpace
for Null, A being Subset of TM st TM | Null is second-countable & Null is finite-ind & A is finite-ind & ind Null <= 0 holds
( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 )

proof end;