:: Small Inductive Dimension of Topological Spaces, Part {II}
:: by Karol P\c{a}k
::
:: Received August 7, 2009
:: 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 b₁ being Subset-Family of X st b₁ is finite-order

proof end;

cluster finite -> finite-order for Element of bool (bool X);

coherence
for b₁ being Subset-Family of X st b₁ is finite holds
b₁ 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 b₁ being ExtReal st
( ( for Gx being Subset-Family of X st b₁ + 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 = b₁ + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) & ( not Fx is finite-order implies ex b₁ being ExtReal st b₁ = +infty ) )

proof end;

uniqueness
for b₁, b₂ being ExtReal holds
( ( Fx is finite-order & ( for Gx being Subset-Family of X st b₁ + 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 = b₁ + 1 & ( not meet Gx is empty or Gx is empty ) ) & ( for Gx being Subset-Family of X st b₂ + 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 = b₂ + 1 & ( not meet Gx is empty or Gx is empty ) ) implies b₁ = b₂ ) & ( not Fx is finite-order & b₁ = +infty & b₂ = +infty implies b₁ = b₂ ) )

proof end;

consistency
for b₁ 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 b₃ being ExtReal holds
( ( Fx is finite-order implies ( b₃ = order Fx iff ( ( for Gx being Subset-Family of X st b₃ + 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 = b₃ + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) ) & ( not Fx is finite-order implies ( b₃ = order Fx iff b₃ = +infty ) ) );

registration

let X be set ;
let F be finite-order Subset-Family of X;

cluster (order F) + 1 -> natural ;

coherence
(order F) + 1 is natural

proof end;

cluster order F -> integer ;

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 b₁ being Subset of TM st b₁ = A \/ B holds
b₁ 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
[:TM1,TM2:] is with_finite_small_inductive_dimension

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;

:: Wprowadzenie do topologii 3.4.10

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 (Euclid 1)
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 (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1)
by EUCLID:def 8;

theorem Th18: :: TOPDIM_2:18

for U being Point of (TOP-REAL 1)
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 b₁ being Subset of TM st b₁ is countable holds
b₁ is finite-ind

proof end;

end;

Lm7: ( TOP-REAL 0 is finite-ind & ind (TOP-REAL 0) = 0 )

proof end;

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

proof end;

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

proof end;

registration

let n be Nat;

cluster TOP-REAL n -> finite-ind ;

coherence
TOP-REAL n is with_finite_small_inductive_dimension by Lm9;

end;

theorem :: TOPDIM_2:20

for n being Nat st n <= 1 holds
ind (TOP-REAL n) = n

proof end;

theorem :: TOPDIM_2:21

for n being Nat holds ind (TOP-REAL n) <= 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;

::Wprowadzenie do topologii Th 3.4.13

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;

::Wprowadzenie do topologii Lm 3.4.17

theorem :: TOPDIM_2:24

for n being Nat
for TM being metrizable TopSpace st TM is finite-ind holds
for A being Subset of TM st ind (A `) <= n & TM | (A `) is second-countable holds
for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )

proof end;