:: Small {I}nductive {D}imension of {T}opological {S}paces :: by Karol P\c{a}k :: :: Received June 29, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users begin theorem Th1: :: TOPDIM_1:1 for T being TopSpace for B, A being Subset of T for F being Subset of (T | A) st F = B /\ A holds Fr F c= (Fr B) /\ A proofend; 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 ) ) proofend; :: 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 b1 being SetSequence of (bool the carrier of T) st for A being Subset of T for n being Nat holds ( b1 . 0 = {({} T)} & ( not A in b1 . (n + 1) or A in b1 . 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 b1 . n ) ) & ( ( A in b1 . 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 b1 . n ) ) implies A in b1 . (n + 1) ) ) proofend; uniqueness for b1, b2 being SetSequence of (bool the carrier of T) st ( for A being Subset of T for n being Nat holds ( b1 . 0 = {({} T)} & ( not A in b1 . (n + 1) or A in b1 . 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 b1 . n ) ) & ( ( A in b1 . 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 b1 . n ) ) implies A in b1 . (n + 1) ) ) ) & ( for A being Subset of T for n being Nat holds ( b2 . 0 = {({} T)} & ( not A in b2 . (n + 1) or A in b2 . 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 b2 . n ) ) & ( ( A in b2 . 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 b2 . n ) ) implies A in b2 . (n + 1) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines Seq_of_ind TOPDIM_1:def_1_:_ for T being TopSpace for b2 being SetSequence of (bool the carrier of T) holds ( b2 = Seq_of_ind T iff for A being Subset of T for n being Nat holds ( b2 . 0 = {({} T)} & ( not A in b2 . (n + 1) or A in b2 . 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 b2 . n ) ) & ( ( A in b2 . 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 b2 . n ) ) implies A in b2 . (n + 1) ) ) ); registration let T be TopSpace; cluster Seq_of_ind T -> non-descending ; coherence Seq_of_ind T is non-descending proofend; 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 ) proofend; definition let T be TopSpace; let A be Subset of T; attrA 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; attrG is with_finite_small_inductive_dimension means :Def3: :: TOPDIM_1:def 3 ex n being Nat st G c= (Seq_of_ind T) . n; end; :: deftheorem Def3 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 Th4: :: 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 proofend; 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) ) proofend; registration let T be TopSpace; cluster finite -> finite-ind for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is finite holds b1 is finite-ind by Lm1; cluster empty -> finite-ind for Element of bool (bool the carrier of T); coherence for b1 being Subset-Family of T st b1 is empty holds b1 is finite-ind proofend; cluster non empty finite-ind for Element of bool (bool the carrier of T); existence ex b1 being Subset-Family of T st ( not b1 is empty & b1 is finite-ind ) proofend; end; registration let T be non empty TopSpace; cluster non empty finite-ind for Element of bool the carrier of T; existence ex b1 being Subset of T st ( not b1 is empty & b1 is finite-ind ) proofend; end; definition let T be TopSpace; attrT 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 b1 being TopSpace st b1 is empty holds b1 is finite-ind proofend; end; Lm2: for X being set holds X in (Seq_of_ind (1TopSp X)) . 1 proofend; registration let X be set ; cluster 1TopSp X -> finite-ind ; coherence 1TopSp X is with_finite_small_inductive_dimension proofend; end; registration cluster non empty TopSpace-like finite-ind for TopStruct ; existence ex b1 being TopSpace st ( not b1 is empty & b1 is finite-ind ) proofend; end; begin definition let T be TopSpace; let A be Subset of T; assume B1: 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 b1 being Integer st ( A in (Seq_of_ind T) . (b1 + 1) & not A in (Seq_of_ind T) . b1 ) proofend; uniqueness for b1, b2 being Integer st A in (Seq_of_ind T) . (b1 + 1) & not A in (Seq_of_ind T) . b1 & A in (Seq_of_ind T) . (b2 + 1) & not A in (Seq_of_ind T) . b2 holds b1 = b2 proofend; 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 b3 being Integer holds ( b3 = ind A iff ( A in (Seq_of_ind T) . (b3 + 1) & not A in (Seq_of_ind T) . b3 ) ); theorem Th5: :: TOPDIM_1:5 for T being TopSpace for Af being finite-ind Subset of T holds - 1 <= ind Af proofend; 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 ) proofend; Lm3: for T being TopSpace for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat proofend; 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 proofend; 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 ) proofend; theorem :: TOPDIM_1:8 for T being TopSpace for A being finite Subset of T holds ind A < card A proofend; 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 ) ) proofend; definition let T be TopSpace; let G be Subset-Family of T; assume B1: 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 b1 being Integer st ( G c= (Seq_of_ind T) . (b1 + 1) & - 1 <= b1 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds b1 <= i ) ) proofend; uniqueness for b1, b2 being Integer st G c= (Seq_of_ind T) . (b1 + 1) & - 1 <= b1 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds b1 <= i ) & G c= (Seq_of_ind T) . (b2 + 1) & - 1 <= b2 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds b2 <= i ) holds b1 = b2 proofend; 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 b3 being Integer holds ( b3 = ind G iff ( G c= (Seq_of_ind T) . (b3 + 1) & - 1 <= b3 & ( for i being Integer st - 1 <= i & G c= (Seq_of_ind T) . (i + 1) holds b3 <= 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)} ) proofend; 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 ) ) ) ) proofend; 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 ) proofend; 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 ) proofend; registration let T be TopSpace; let G1, G2 be finite-ind Subset-Family of T; clusterG1 \/ G2 -> finite-ind for Subset-Family of T; coherence for b1 being Subset-Family of T st b1 = G1 \/ G2 holds b1 is with_finite_small_inductive_dimension proofend; 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 proofend; end; theorem :: TOPDIM_1:14 for X being non empty set holds ind (1TopSp X) = 0 proofend; 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 proofend; 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 ) ) proofend; Lm5: for T being TopSpace for Af being finite-ind Subset of T holds ( T | Af is finite-ind & ind (T | Af) = ind Af ) proofend; Lm6: for Tf being finite-ind TopSpace for A being Subset of Tf holds ( Tf | A is finite-ind & ind (Tf | A) <= ind Tf ) proofend; Lm7: for T being TopSpace for A being Subset of T st T is finite-ind holds A is finite-ind proofend; begin registration let Tf be finite-ind TopSpace; cluster -> finite-ind for Element of bool the carrier of Tf; coherence for b1 being Subset of Tf holds b1 is finite-ind by Lm7; end; registration let T be TopSpace; let Af be finite-ind Subset of T; clusterT | 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; Lm8: for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is finite-ind holds ( T2 is finite-ind & ind T2 <= ind T1 ) proofend; 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 ) ) proofend; :: 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 ) ) proofend; 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 ) proofend; 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 proofend; 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:] ) proofend; 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 ) proofend; 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 ) proofend; begin :: 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 ) ) proofend; :: 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 ) proofend; 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) ) ) ) proofend; :: 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 ) proofend; :: 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 ) proofend; 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 ) proofend; :: 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 ) proofend; :: 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 ) ) proofend; :: 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 ) proofend; :: 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 ) proofend;