:: Small Inductive Dimension of Topological Spaces, Part {II} :: by Karol P\c{a}k :: :: Received August 7, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users begin definition let X be set ; let Fx be Subset-Family of X; attrFx 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 proofend; 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 proofend; end; definition let X be set ; let Fx be Subset-Family of X; func order Fx -> ext-real number 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 ext-real number 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 ext-real number st b1 = +infty ) ) proofend; uniqueness for b1, b2 being ext-real number 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 ) ) proofend; consistency for b1 being ext-real number 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 ext-real number 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(order F) + 1 -> natural ; coherence (order F) + 1 is natural proofend; cluster order F -> ext-real integer ; coherence order F is integer proofend; 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 proofend; 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 proofend; 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 proofend; begin Lm1: for T being TopSpace for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat proofend; 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 ) proofend; 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 ) ) ) proofend; ::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 ) proofend; ::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 ) ) proofend; ::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 ) proofend; 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 ) proofend; registration let TM be second-countable metrizable TopSpace; let A, B be finite-ind Subset of TM; clusterA \/ 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 proofend; 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):] proofend; 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) ) proofend; 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 proofend; 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 ) proofend; ::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 ) proofend; ::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 ) ) proofend; ::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 ) ) proofend; ::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 TM2, TM1 being second-countable finite-ind metrizable TopSpace st ind TM2 = 0 holds ind [:TM1,TM2:] = ind TM1 proofend; begin theorem Th17: :: TOPDIM_2:17 for u being Point of (Euclid 1) for u1, r being real number st <*u1*> = u holds cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } proofend; 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 u1, r being real number st <*u1*> = U & r > 0 holds Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>} proofend; 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 ) proofend; 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 proofend; end; Lm7: ( TOP-REAL 0 is finite-ind & ind (TOP-REAL 0) = 0 ) proofend; Lm8: ( TOP-REAL 1 is finite-ind & ind (TOP-REAL 1) = 1 ) proofend; Lm9: for n being Nat holds ( TOP-REAL n is finite-ind & ind (TOP-REAL n) <= n ) proofend; 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 proofend; 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 ) proofend; ::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 ) ) proofend; :: 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 ) proofend; ::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 ) proofend;