:: by Karol P\c{a}k

::

:: Received August 7, 2009

:: Copyright (c) 2009-2016 Association of Mizar Users

definition

let X be set ;

let Fx be Subset-Family of X;

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

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 ;

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

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 ;

existence

ex b_{1} being Subset-Family of X st b_{1} is finite-order

for b_{1} being Subset-Family of X st b_{1} is finite holds

b_{1} is finite-order

end;
existence

ex b

proof end;

coherence for b

b

proof end;

definition

let X be set ;

let Fx be Subset-Family of X;

( ( Fx is finite-order implies ex b_{1} being ExtReal st

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

for b_{1}, b_{2} being ExtReal holds

( ( Fx is finite-order & ( for Gx being Subset-Family of X st b_{1} + 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} + 1 & ( not meet Gx is empty or Gx is empty ) ) & ( for Gx being Subset-Family of X st b_{2} + 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_{2} + 1 & ( not meet Gx is empty or Gx is empty ) ) implies b_{1} = b_{2} ) & ( not Fx is finite-order & b_{1} = +infty & b_{2} = +infty implies b_{1} = b_{2} ) )

for b_{1} being ExtReal holds verum
;

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

( ( Fx is finite-order implies ex b

( ( for Gx being Subset-Family of X st b

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = b

proof end;

uniqueness for b

( ( Fx is finite-order & ( for Gx being Subset-Family of X st b

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = b

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = b

proof end;

consistency for b

:: deftheorem Def2 defines order TOPDIM_2:def 2 :

for X being set

for Fx being Subset-Family of X

for b_{3} being ExtReal holds

( ( Fx is finite-order implies ( b_{3} = order Fx iff ( ( for Gx being Subset-Family of X st b_{3} + 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_{3} + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) ) & ( not Fx is finite-order implies ( b_{3} = order Fx iff b_{3} = +infty ) ) );

for X being set

for Fx being Subset-Family of X

for b

( ( Fx is finite-order implies ( b

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = b

registration

let X be set ;

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

coherence

(order F) + 1 is natural

order F is integer

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

coherence

(order F) + 1 is natural

proof end;

coherence order F is integer

proof 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

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

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

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;

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 )

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

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

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 )

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;

coherence

for b_{1} being Subset of TM st b_{1} = A \/ B holds

b_{1} is with_finite_small_inductive_dimension

end;
let A, B be finite-ind Subset of TM;

coherence

for b

b

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

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

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;

coherence

[:TM1,TM2:] is with_finite_small_inductive_dimension

end;
coherence

[:TM1,TM2:] is with_finite_small_inductive_dimension

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

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 )

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

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

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;

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

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 ) }

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)*>}

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 )

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;

coherence

for b_{1} being Subset of TM st b_{1} is countable holds

b_{1} is finite-ind

end;
coherence

for b

b

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

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

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 )

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 )

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;