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

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 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 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 Nat st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) & ( for x being Real holds
( x in b₂ iff ex i being Nat st
( i <= 2 |^ n & x = i / (2 |^ n) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines dyadic URYSOHN1:def 1 :
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 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 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 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 Nat st a in dyadic n ) ) & ( for a being Real holds
( a in b₂ iff ex n being Nat st a in dyadic n ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines DYADIC URYSOHN1:def 2 :
for b₁ being Subset of REAL holds
( b₁ = DYADIC iff for a being Real holds
( a in b₁ iff ex n being 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);

theorem Th1: :: URYSOHN1:1

for n being 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 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 Nat st i in dom b₁ holds
b₁ . i = (i - 1) / (2 |^ n) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st dom b₁ = Seg ((2 |^ n) + 1) & ( for i being Nat st i in dom b₁ holds
b₁ . i = (i - 1) / (2 |^ n) ) & dom b₂ = Seg ((2 |^ n) + 1) & ( for i being Nat st i in dom b₂ holds
b₂ . i = (i - 1) / (2 |^ n) ) holds
b₁ = b₂

proof end;

end;

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

theorem :: URYSOHN1:4

for n being 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 Nat holds dyadic n c= dyadic (n + 1)

proof end;

theorem Th6: :: URYSOHN1:6

for n being Nat holds
( 0 in dyadic n & 1 in dyadic n )

proof end;

theorem Th7: :: URYSOHN1:7

for n, i being 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 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 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 -> Nat means :Def5: :: URYSOHN1:def 5
x = it / (2 |^ n);

existence
ex b₁ being Nat st x = b₁ / (2 |^ n)

proof end;

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

proof end;

end;

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

theorem Th10: :: URYSOHN1:10

for n being 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 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 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 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 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 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 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;

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 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 6 :
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 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 :: 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 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;

::
:: 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 b₁ being Subset of T st
( b₁ <> {} & b₁ is open & Cl A c= b₁ & Cl b₁ 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 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: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 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;