:: Small Inductive Dimension of Topological Spaces, Part {II}
:: by Karol P\c{a}k
::
:: Copyright (c) 2009-2021 Association of Mizar Users

definition
let X be set ;
let Fx be Subset-Family of X;
attr Fx is finite-order means :Def1: :: TOPDIM_2:def 1
ex n being Nat st
for Gx being Subset-Family of X st Gx c= Fx & n in card Gx holds
meet Gx is empty ;
end;

:: deftheorem Def1 defines finite-order TOPDIM_2:def 1 :
for X being set
for Fx being Subset-Family of X holds
( Fx is finite-order iff ex n being Nat st
for Gx being Subset-Family of X st Gx c= Fx & n in card Gx holds
meet Gx is empty );

registration
let X be set ;
cluster finite-order for Element of bool (bool X);
existence
ex b1 being Subset-Family of X st b1 is finite-order
proof end;
cluster finite -> finite-order for Element of bool (bool X);
coherence
for b1 being Subset-Family of X st b1 is finite holds
b1 is finite-order
proof end;
end;

definition
let X be set ;
let Fx be Subset-Family of X;
func order Fx -> ExtReal means :Def2: :: TOPDIM_2:def 2
( ( for Gx being Subset-Family of X st it + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = it + 1 & ( not meet Gx is empty or Gx is empty ) ) ) if Fx is finite-order
otherwise it = +infty ;
existence
( ( Fx is finite-order implies ex b1 being ExtReal st
( ( for Gx being Subset-Family of X st b1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b1 + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) & ( not Fx is finite-order implies ex b1 being ExtReal st b1 = +infty ) )
proof end;
uniqueness
for b1, b2 being ExtReal holds
( ( Fx is finite-order & ( for Gx being Subset-Family of X st b1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b1 + 1 & ( not meet Gx is empty or Gx is empty ) ) & ( for Gx being Subset-Family of X st b2 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b2 + 1 & ( not meet Gx is empty or Gx is empty ) ) implies b1 = b2 ) & ( not Fx is finite-order & b1 = +infty & b2 = +infty implies b1 = b2 ) )
proof end;
consistency
for b1 being ExtReal holds verum
;
end;

:: deftheorem Def2 defines order TOPDIM_2:def 2 :
for X being set
for Fx being Subset-Family of X
for b3 being ExtReal holds
( ( Fx is finite-order implies ( b3 = order Fx iff ( ( for Gx being Subset-Family of X st b3 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b3 + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) ) & ( not Fx is finite-order implies ( b3 = order Fx iff b3 = +infty ) ) );

registration
let X be set ;
let F be finite-order Subset-Family of X;
cluster () + 1 -> natural ;
coherence
() + 1 is natural
proof end;
coherence
order F is integer
proof end;
end;

theorem Th1: :: TOPDIM_2:1
for n being Nat
for X being set
for Fx being Subset-Family of X st order Fx <= n holds
Fx is finite-order
proof end;

theorem :: TOPDIM_2:2
for n being Nat
for X being set
for Fx being Subset-Family of X st order Fx <= n holds
for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds
meet Gx is empty
proof end;

theorem Th3: :: TOPDIM_2:3
for n being Nat
for X being set
for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds
meet G is empty ) holds
order Fx <= n
proof end;

Lm1: for T being TopSpace
for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat

proof end;

Lm2: for n being Nat
for T being TopSpace
for g being SetSequence of T st ( for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) holds
ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G )

proof end;

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 finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & 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 ) ) )

proof end;

::Teoria wymiaru Th 1.5.3
theorem :: TOPDIM_2:4
for n being Nat
for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st
( F is closed & F is Cover of TM & F is countable & F is finite-ind & ind F <= n ) holds
( TM is finite-ind & ind TM <= n ) by Lm3;

::Teoria wymiaru Th 1.5.5
theorem Th5: :: TOPDIM_2:5
for TM being metrizable TopSpace
for I being Integer
for A, B being finite-ind Subset of TM st A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I holds
( ind (A \/ B) <= I & A \/ B is finite-ind )
proof end;

::Teoria wymiaru Th 1.5.7 "=>"
theorem :: TOPDIM_2:6
for n being Nat
for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= n holds
ex A, B being Subset of TM st
( [#] TM = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) by Lm3;

::Teoria wymiaru Th 1.5.8 "=>"
theorem Th7: :: TOPDIM_2:7
for I being Integer
for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= I holds
ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds
A = B ) )
proof end;

::Teoria wymiaru Th 1.5.8 "<="
theorem Th8: :: TOPDIM_2:8
for I being Integer
for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 ) holds
( TM is finite-ind & ind TM <= I )
proof end;

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

proof end;

registration
let TM be second-countable metrizable TopSpace;
let A, B be finite-ind Subset of TM;
cluster A \/ B -> finite-ind for Subset of TM;
coherence
for b1 being Subset of TM st b1 = A \/ B holds
b1 is with_finite_small_inductive_dimension
proof end;
end;

::Teoria wymiaru Th 1.5.10
theorem :: TOPDIM_2:9
for TM being metrizable TopSpace
for A, B being Subset of TM st A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable holds
( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) by Lm4;

theorem Th10: :: TOPDIM_2:10
for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 holds Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):]
proof end;

Lm5: for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) holds
( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )

proof end;

registration
let TM1, TM2 be second-countable finite-ind metrizable TopSpace;
cluster [:TM1,TM2:] -> finite-ind ;
coherence
proof end;
end;

::Teoria wymiaru Th 1.5.12
theorem Th11: :: TOPDIM_2:11
for n being Nat
for TM being metrizable TopSpace
for A, B being Subset of TM st A is closed & B is closed & A misses B holds
for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds
ex L being Subset of TM st
( L separates A,B & ind (L /\ H) <= n - 1 )
proof end;

::Teoria wymiaru Th 1.5.13
theorem :: TOPDIM_2:12
for n being Nat
for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable & ind TM <= n holds
for A, B being Subset of TM st A is closed & B is closed & A misses B holds
ex L being Subset of TM st
( L separates A,B & ind L <= n - 1 )
proof end;

::Teoria wymiaru Th 1.5.14
theorem Th13: :: TOPDIM_2:13
for n being Nat
for TM being metrizable TopSpace
for H being Subset of TM st TM | H is second-countable holds
( ( H is finite-ind & ind H <= n ) 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 & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) )
proof end;

::Teoria wymiaru Th 1.5.15
theorem :: TOPDIM_2:14
for n being Nat
for TM being metrizable TopSpace
for H being Subset of TM st TM | H is second-countable holds
( ( H is finite-ind & ind H <= n ) iff ex Bas being Basis of TM st
for A being Subset of TM st A in Bas holds
( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) )
proof end;

::Teoria wymiaru Th 1.5.16
theorem :: TOPDIM_2:15
for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) holds
ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) by Lm5;

theorem :: TOPDIM_2:16
for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ind TM2 = 0 holds
ind [:TM1,TM2:] = ind TM1
proof end;

theorem Th17: :: TOPDIM_2:17
for u being Point of ()
for r, u1 being Real st <*u1*> = u holds
cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
proof end;

Lm6: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr ()
by EUCLID:def 8;

theorem Th18: :: TOPDIM_2:18
for U being Point of ()
for r, u1 being Real st <*u1*> = U & r > 0 holds
Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>}
proof end;

theorem Th19: :: TOPDIM_2:19
for T being TopSpace
for A being countable Subset of T st T | A is T_4 holds
( A is finite-ind & ind A <= 0 )
proof end;

registration
let TM be metrizable TopSpace;
cluster countable -> finite-ind for Element of bool the carrier of TM;
coherence
for b1 being Subset of TM st b1 is countable holds
b1 is finite-ind
proof end;
end;

Lm7:
proof end;

Lm8: ( TOP-REAL 1 is finite-ind & ind () = 1 )
proof end;

Lm9: for n being Nat holds
( TOP-REAL n is finite-ind & ind () <= n )

proof end;

registration
let n be Nat;
coherence by Lm9;
end;

theorem :: TOPDIM_2:20
for n being Nat st n <= 1 holds
ind () = n
proof end;

theorem :: TOPDIM_2:21
for n being Nat holds ind () <= n by Lm9;

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

proof end;

theorem Th22: :: TOPDIM_2:22
for TM being metrizable TopSpace
for A being Subset of TM st TM | A is second-countable & TM | A is finite-ind & ind A <= 0 holds
for F being finite Subset-Family of TM st F is open & F is Cover of A holds
ex g being Function of F,(bool the carrier of TM) st
( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) )
proof end;

:: Wprowadzenie do topologii Th 3.4.14
theorem :: TOPDIM_2:23
for n being Nat
for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= n holds
for F being finite Subset-Family of TM st F is open & F is Cover of TM holds
ex G being finite Subset-Family of TM st
( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )
proof end;

for A being Subset of TM st ind (A ) <= n & TM | (A ) is second-countable holds