:: Dyadic Numbers and $T_4$ Topological Spaces :: by J\'ozef Bia\las and Yatsuka Nakamura :: :: Received July 29, 1995 :: Copyright (c) 1995-2012 Association of Mizar Users begin definition let n be Nat; func dyadic n -> Subset of REAL means :Def1: :: URYSOHN1:def 1 for x being Real holds ( x in it iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ); existence ex b1 being Subset of REAL st for x being Real holds ( x in b1 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) proofend; uniqueness for b1, b2 being Subset of REAL st ( for x being Real holds ( x in b1 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds ( x in b2 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines dyadic URYSOHN1:def_1_:_ for n being Nat for b2 being Subset of REAL holds ( b2 = dyadic n iff for x being Real holds ( x in b2 iff ex i being Element of NAT st ( i <= 2 |^ n & x = i / (2 |^ n) ) ) ); definition func DYADIC -> Subset of REAL means :Def2: :: URYSOHN1:def 2 for a being Real holds ( a in it iff ex n being Element of NAT st a in dyadic n ); existence ex b1 being Subset of REAL st for a being Real holds ( a in b1 iff ex n being Element of NAT st a in dyadic n ) proofend; uniqueness for b1, b2 being Subset of REAL st ( for a being Real holds ( a in b1 iff ex n being Element of NAT st a in dyadic n ) ) & ( for a being Real holds ( a in b2 iff ex n being Element of NAT st a in dyadic n ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines DYADIC URYSOHN1:def_2_:_ for b1 being Subset of REAL holds ( b1 = DYADIC iff for a being Real holds ( a in b1 iff ex n being Element of NAT st a in dyadic n ) ); definition func DOM -> Subset of REAL equals :: URYSOHN1:def 3 ((halfline 0) \/ DYADIC) \/ (right_open_halfline 1); coherence ((halfline 0) \/ DYADIC) \/ (right_open_halfline 1) is Subset of REAL ; end; :: deftheorem defines DOM URYSOHN1:def_3_:_ DOM = ((halfline 0) \/ DYADIC) \/ (right_open_halfline 1); definition let T be TopSpace; let A be non empty Subset of REAL; let F be Function of A,(bool the carrier of T); let r be Element of A; :: original:. redefine funcF . r -> Subset of T; coherence F . r is Subset of T proofend; end; theorem Th1: :: URYSOHN1:1 for n being Element of NAT for x being Real st x in dyadic n holds ( 0 <= x & x <= 1 ) proofend; theorem Th2: :: URYSOHN1:2 dyadic 0 = {0,1} proofend; theorem :: URYSOHN1:3 dyadic 1 = {0,(1 / 2),1} proofend; registration let n be Nat; cluster dyadic n -> non empty ; coherence not dyadic n is empty proofend; end; definition let n be Nat; func dyad n -> FinSequence means :Def4: :: URYSOHN1:def 4 ( dom it = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom it holds it . i = (i - 1) / (2 |^ n) ) ); existence ex b1 being FinSequence st ( dom b1 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b1 holds b1 . i = (i - 1) / (2 |^ n) ) ) proofend; uniqueness for b1, b2 being FinSequence st dom b1 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b1 holds b1 . i = (i - 1) / (2 |^ n) ) & dom b2 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b2 holds b2 . i = (i - 1) / (2 |^ n) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines dyad URYSOHN1:def_4_:_ for n being Nat for b2 being FinSequence holds ( b2 = dyad n iff ( dom b2 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b2 holds b2 . i = (i - 1) / (2 |^ n) ) ) ); theorem :: URYSOHN1:4 for n being Element of NAT holds ( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n ) proofend; registration cluster DYADIC -> non empty ; coherence not DYADIC is empty proofend; end; registration cluster DOM -> non empty ; coherence not DOM is empty ; end; theorem Th5: :: URYSOHN1:5 for n being Element of NAT holds dyadic n c= dyadic (n + 1) proofend; theorem Th6: :: URYSOHN1:6 for n being Element of NAT holds ( 0 in dyadic n & 1 in dyadic n ) proofend; theorem Th7: :: URYSOHN1:7 for n, i being Element of NAT st 0 < i & i <= 2 |^ n holds ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) proofend; theorem Th8: :: URYSOHN1:8 for n, i being Element of NAT st 0 <= i & i < 2 |^ n holds ((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) proofend; theorem Th9: :: URYSOHN1:9 for n being Element of NAT holds 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) proofend; definition let n be Nat; let x be Element of dyadic n; func axis x -> Element of NAT means :Def5: :: URYSOHN1:def 5 x = it / (2 |^ n); existence ex b1 being Element of NAT st x = b1 / (2 |^ n) proofend; uniqueness for b1, b2 being Element of NAT st x = b1 / (2 |^ n) & x = b2 / (2 |^ n) holds b1 = b2 proofend; end; :: deftheorem Def5 defines axis URYSOHN1:def_5_:_ for n being Nat for x being Element of dyadic n for b3 being Element of NAT holds ( b3 = axis x iff x = b3 / (2 |^ n) ); theorem Th10: :: URYSOHN1:10 for n being Element of NAT for x being Element of dyadic n holds ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n ) proofend; theorem :: URYSOHN1:11 for n being Element of NAT for x being Element of dyadic n holds ( ((axis x) - 1) / (2 |^ n) < x & x < ((axis x) + 1) / (2 |^ n) ) proofend; theorem Th12: :: URYSOHN1:12 for n being Element of NAT for x being Element of dyadic n holds ((axis x) - 1) / (2 |^ n) < ((axis x) + 1) / (2 |^ n) proofend; theorem Th13: :: URYSOHN1:13 for n being Element of NAT for x being Element of dyadic (n + 1) st not x in dyadic n holds ( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ) proofend; theorem Th14: :: URYSOHN1:14 for n being Element of NAT for x1, x2 being Element of dyadic n st x1 < x2 holds axis x1 < axis x2 proofend; theorem Th15: :: URYSOHN1:15 for n being Element of NAT for x1, x2 being Element of dyadic n st x1 < x2 holds ( x1 <= ((axis x2) - 1) / (2 |^ n) & ((axis x1) + 1) / (2 |^ n) <= x2 ) proofend; theorem Th16: :: URYSOHN1:16 for n being Element of NAT for x1, x2 being Element of dyadic (n + 1) st x1 < x2 & not x1 in dyadic n & not x2 in dyadic n holds ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) proofend; begin notation let T be non empty TopSpace; let x be Point of T; synonym Nbhd of x,T for a_neighborhood of x; end; definition let T be non empty TopSpace; let x be Point of T; redefine mode a_neighborhood of x means :: URYSOHN1:def 6 ex A being Subset of T st ( A is open & x in A & A c= it ); compatibility for b1 being Element of bool the carrier of T holds ( b1 is Nbhd of x,T iff ex A being Subset of T st ( A is open & x in A & A c= b1 ) ) proofend; end; :: deftheorem defines Nbhd URYSOHN1:def_6_:_ for T being non empty TopSpace for x being Point of T for b3 being Element of bool the carrier of T holds ( b3 is Nbhd of x,T iff ex A being Subset of T st ( A is open & x in A & A c= b3 ) ); theorem Th17: :: URYSOHN1:17 for T being non empty TopSpace for A being Subset of T holds ( A is open iff for x being Point of T st x in A holds ex B being Nbhd of x,T st B c= A ) proofend; theorem :: URYSOHN1:18 for T being non empty TopSpace for A being Subset of T st ( for x being Point of T st x in A holds A is Nbhd of x,T ) holds A is open proofend; definition let T be TopSpace; redefine attr T is T_1 means :Def7: :: URYSOHN1:def 7 for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ); compatibility ( T is T_1 iff for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) ) proofend; end; :: deftheorem Def7 defines T_1 URYSOHN1:def_7_:_ for T being TopSpace holds ( T is T_1 iff for p, q being Point of T st not p = q holds ex W, V being Subset of T st ( W is open & V is open & p in W & not q in W & q in V & not p in V ) ); theorem Th19: :: URYSOHN1:19 for T being non empty TopSpace holds ( T is T_1 iff for p being Point of T holds {p} is closed ) proofend; theorem Th20: :: URYSOHN1:20 for T being non empty TopSpace st T is normal holds for A, B being open Subset of T st A <> {} & Cl A c= B holds ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) proofend; theorem :: URYSOHN1:21 for T being non empty TopSpace holds ( T is regular iff for A being open Subset of T for p being Point of T st p in A holds ex B being open Subset of T st ( p in B & Cl B c= A ) ) proofend; theorem :: URYSOHN1:22 for T being non empty TopSpace st T is normal & T is T_1 holds for A being open Subset of T st A <> {} holds ex B being Subset of T st ( B <> {} & Cl B c= A ) proofend; theorem :: URYSOHN1:23 for T being non empty TopSpace st T is normal holds for A, B being Subset of T st A is open & B is closed & B <> {} & B c= A holds ex C being Subset of T st ( C is open & B c= C & Cl C c= A ) proofend; begin :: :: Some increasing family of sets in normal space :: definition let T be non empty TopSpace; let A, B be Subset of T; assume A1: ( T is normal & A <> {} & A is open & B is open & Cl A c= B ) ; mode Between of A,B -> Subset of T means :Def8: :: URYSOHN1:def 8 ( it <> {} & it is open & Cl A c= it & Cl it c= B ); existence ex b1 being Subset of T st ( b1 <> {} & b1 is open & Cl A c= b1 & Cl b1 c= B ) by A1, Th20; end; :: deftheorem Def8 defines Between URYSOHN1:def_8_:_ for T being non empty TopSpace for A, B being Subset of T st T is normal & A <> {} & A is open & B is open & Cl A c= B holds for b4 being Subset of T holds ( b4 is Between of A,B iff ( b4 <> {} & b4 is open & Cl A c= b4 & Cl b4 c= B ) ); theorem :: URYSOHN1:24 for T being non empty TopSpace st T is normal holds for A, B being closed Subset of T st A <> {} holds for n being Element of NAT for G being Function of (dyadic n),(bool the carrier of T) st A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds ( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) ) holds ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) proofend;