:: 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) ) )
proof end;
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
proof end;
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 )
proof end;
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
proof end;
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 func F . r -> Subset of T;
coherence
F . r is Subset of T
proof end;
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 )
proof end;

theorem Th2: :: URYSOHN1:2
dyadic 0 = {0,1}
proof end;

theorem :: URYSOHN1:3
dyadic 1 = {0,(1 / 2),1}
proof end;

registration
let n be Nat;
cluster dyadic n -> non empty ;
coherence
not dyadic n is empty
proof end;
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) ) )
proof end;
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
proof end;
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 )
proof end;

registration
cluster DYADIC -> non empty ;
coherence
not DYADIC is empty
proof end;
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)
proof end;

theorem Th6: :: URYSOHN1:6
for n being Element of NAT holds
( 0 in dyadic n & 1 in dyadic n )
proof end;

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

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

theorem Th9: :: URYSOHN1:9
for n being Element of NAT holds 1 / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)
proof end;

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)
proof end;
uniqueness
for b1, b2 being Element of NAT st x = b1 / (2 |^ n) & x = b2 / (2 |^ n) holds
b1 = b2
proof end;
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 )
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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