:: Dyadic Numbers and $T_4$ Topological Spaces
:: by J\'ozef Bia\las and Yatsuka Nakamura
::
:: Received July 29, 1995
:: Copyright (c) 1995-2011 Association of Mizar Users

begin

definition

canceled;
canceled;
let n be Nat;
func dyadic n -> Subset of REAL means :Def3: :: URYSOHN1:def 3
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 b₁ being Subset of REAL st
for x being Real holds
( x in b₁ iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) )

proof end;

uniqueness
for b₁, b₂ being Subset of REAL st ( for x being Real holds
( x in b₁ iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds
( x in b₂ iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem URYSOHN1:def 1 :
canceled;

:: deftheorem URYSOHN1:def 2 :
canceled;

:: deftheorem Def3 defines dyadic URYSOHN1:def 3 :
for n being Nat
for b₂ being Subset of REAL holds
( b₂ = dyadic n iff for x being Real holds
( x in b₂ iff ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) );

definition

func DYADIC -> Subset of REAL means :Def4: :: URYSOHN1:def 4
for a being Real holds
( a in it iff ex n being Element of NAT st a in dyadic n );
existence
ex b₁ being Subset of REAL st
for a being Real holds
( a in b₁ iff ex n being Element of NAT st a in dyadic n )

proof end;

uniqueness
for b₁, b₂ being Subset of REAL st ( for a being Real holds
( a in b₁ iff ex n being Element of NAT st a in dyadic n ) ) & ( for a being Real holds
( a in b₂ iff ex n being Element of NAT st a in dyadic n ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines DYADIC URYSOHN1:def 4 :
for b₁ being Subset of REAL holds
( b₁ = DYADIC iff for a being Real holds
( a in b₁ iff ex n being Element of NAT st a in dyadic n ) );

definition

func DOM -> Subset of REAL equals :: URYSOHN1:def 5
((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 5 :
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 :: URYSOHN1:1

canceled;

theorem :: URYSOHN1:2

canceled;

theorem :: URYSOHN1:3

canceled;

theorem :: URYSOHN1:4

canceled;

theorem Th5: :: URYSOHN1:5

for n being Element of NAT
for x being Real st x in dyadic n holds
( 0 <= x & x <= 1 )

proof end;

theorem Th6: :: URYSOHN1:6

dyadic 0 = {0,1}

proof end;

theorem :: URYSOHN1:7

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;

theorem :: URYSOHN1:8

canceled;

theorem :: URYSOHN1:9

canceled;

Lm1: for n being Nat ex FS being FinSequence st
( dom FS = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom FS holds
FS . i = (i - 1) / (2 |^ n) ) )

proof end;

definition

let n be Nat;
func dyad n -> FinSequence means :Def6: :: URYSOHN1:def 6
( 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 b₁ being FinSequence st
( dom b₁ = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b₁ holds
b₁ . i = (i - 1) / (2 |^ n) ) ) by Lm1;
uniqueness
for b₁, b₂ being FinSequence st dom b₁ = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b₁ holds
b₁ . i = (i - 1) / (2 |^ n) ) & dom b₂ = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b₂ holds
b₂ . i = (i - 1) / (2 |^ n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines dyad URYSOHN1:def 6 :
for n being Nat
for b₂ being FinSequence holds
( b₂ = dyad n iff ( dom b₂ = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom b₂ holds
b₂ . i = (i - 1) / (2 |^ n) ) ) );

theorem :: URYSOHN1:10

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 Th11: :: URYSOHN1:11

for n being Element of NAT holds dyadic n c= dyadic (n + 1)

proof end;

theorem Th12: :: URYSOHN1:12

for n being Element of NAT holds
( 0 in dyadic n & 1 in dyadic n )

proof end;

theorem Th13: :: URYSOHN1:13

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 Th14: :: URYSOHN1:14

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 Th15: :: URYSOHN1:15

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 :Def7: :: URYSOHN1:def 7
x = it / (2 |^ n);
existence
ex b₁ being Element of NAT st x = b₁ / (2 |^ n)

proof end;

uniqueness
for b₁, b₂ being Element of NAT st x = b₁ / (2 |^ n) & x = b₂ / (2 |^ n) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines axis URYSOHN1:def 7 :
for n being Nat
for x being Element of dyadic n
for b₃ being Element of NAT holds
( b₃ = axis x iff x = b₃ / (2 |^ n) );

theorem Th16: :: URYSOHN1:16

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

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 Th18: :: URYSOHN1:18

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 :: URYSOHN1:19

canceled;

theorem Th20: :: URYSOHN1:20

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 Th21: :: URYSOHN1:21

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 Th22: :: URYSOHN1:22

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 Th23: :: URYSOHN1:23

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 8
ex A being Subset of T st
( A is open & x in A & A c= it );
compatibility
for b₁ being Element of bool the carrier of T holds
( b₁ is Nbhd of x,T iff ex A being Subset of T st
( A is open & x in A & A c= b₁ ) )

proof end;

end;

:: deftheorem defines Nbhd URYSOHN1:def 8 :
for T being non empty TopSpace
for x being Point of T
for b₃ being Element of bool the carrier of T holds
( b₃ is Nbhd of x,T iff ex A being Subset of T st
( A is open & x in A & A c= b₃ ) );

theorem Th24: :: URYSOHN1:24

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

canceled;

theorem :: URYSOHN1:26

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 :Def9: :: URYSOHN1:def 9
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 Def9 defines T_1 URYSOHN1:def 9 :
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 Th27: :: URYSOHN1:27

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 Th28: :: URYSOHN1:28

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

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

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

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

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 :Def10: :: URYSOHN1:def 10
( it <> {} & it is open & Cl A c= it & Cl it c= B );
existence
ex b₁ being Subset of T st
( b₁ <> {} & b₁ is open & Cl A c= b₁ & Cl b₁ c= B ) by A1, Th28;

end;

:: deftheorem Def10 defines Between URYSOHN1:def 10 :
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 b₄ being Subset of T holds
( b₄ is Between of A,B iff ( b₄ <> {} & b₄ is open & Cl A c= b₄ & Cl b₄ c= B ) );

theorem :: URYSOHN1:32

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;