Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

### Dyadic Numbers and T\$_4\$ Topological Spaces

by
Jozef Bialas, and
Yatsuka Nakamura

MML identifier: URYSOHN1
[ Mizar article, MML identifier index ]

```environ

vocabulary GROUP_1, ARYTM_3, PRALG_2, BOOLE, PRE_TOPC, FUNCT_1, FINSEQ_1,
RELAT_1, ARYTM_1, CONNSP_2, TOPS_1, SUBSET_1, SETFAM_1, TARSKI, TOPMETR,
COMPTS_1, URYSOHN1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, DOMAIN_1,
FUNCT_1, FUNCT_2, REAL_1, FINSEQ_1, NAT_1, TOPMETR, COMPTS_1, STRUCT_0,
PRE_TOPC, CARD_4, TOPS_1, CONNSP_2;
constructors DOMAIN_1, REAL_1, NAT_1, TOPMETR, COMPTS_1, CARD_4, TOPS_1,
MEMBERED;
clusters SUBSET_1, STRUCT_0, PRE_TOPC, RELSET_1, TOPS_1, ARYTM_3, XREAL_0,
MEMBERED, ZFMISC_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

definition
func R<0 ->Subset of REAL means
:: URYSOHN1:def 1
for x being Real holds x in it iff x < 0;
end;

definition
func R>1 ->Subset of REAL means
:: URYSOHN1:def 2
for x being Real holds x in it iff 1 < x;
end;

definition
let n be Nat;
func dyadic(n) -> Subset of REAL means
:: URYSOHN1:def 3
for x being Real holds
x in it iff ex i being Nat st (0 <= i & i <= (2|^n) & x = i/(2|^n));
end;

definition
func DYADIC -> Subset of REAL means
:: URYSOHN1:def 4
for a being Real holds a in it iff
ex n being Nat st a in dyadic(n);
end;

definition
func DOM -> Subset of REAL equals
:: URYSOHN1:def 5
end;

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;
redefine func F.r -> Subset of T;
end;

canceled 4;

theorem :: URYSOHN1:5
for n being Nat holds
for x being Real st x in dyadic(n) holds
0 <= x & x <= 1;

theorem :: URYSOHN1:6

theorem :: URYSOHN1:7

definition let n be Nat;
end;

theorem :: URYSOHN1:8
for x, n being Nat holds x|^n is Nat;

theorem :: URYSOHN1:9
for n being Nat holds
ex FS being FinSequence st (dom FS = Seg ((2|^n)+1) &
for i being Nat st i in dom FS holds FS.i = (i-1)/(2|^n));

definition
let n be Nat;
:: URYSOHN1:def 6
dom it = Seg((2|^n)+1) &
for i being Nat st i in dom it holds it.i = (i-1)/(2|^n);
end;

theorem :: URYSOHN1:10
for n being Nat holds

definition
end;

definition
cluster DOM -> non empty;
end;

theorem :: URYSOHN1:11

theorem :: URYSOHN1:12
for n being Nat holds

theorem :: URYSOHN1:13
for n,i being Nat st 0 < i & i <= 2|^n holds

theorem :: URYSOHN1:14
for n,i being Nat st 0 <= i & i < 2|^n holds

theorem :: URYSOHN1:15

definition
let n be Nat;
let x be Element of dyadic(n);
func axis(x,n) -> Nat means
:: URYSOHN1:def 7
x = it/(2|^n);
end;

theorem :: URYSOHN1:16
for n being Nat holds
for x being Element of dyadic(n) holds
x = axis(x,n)/(2|^n) & 0 <= axis(x,n) & axis(x,n) <= (2|^n);

theorem :: URYSOHN1:17
for n being Nat holds
for x being Element of dyadic(n) holds
(axis(x,n)-1)/(2|^n) < x & x < (axis(x,n)+1)/(2|^n);

theorem :: URYSOHN1:18
for n being Nat holds
for x being Element of dyadic(n) holds
((axis(x,n)-1)/(2|^n) < (axis(x,n)+1)/(2|^n));

canceled;

theorem :: URYSOHN1:20
for n being Nat holds
for x being Element of dyadic(n+1) holds

theorem :: URYSOHN1:21
for n being Nat holds
for x1,x2 being Element of dyadic(n) st x1 < x2 holds
axis(x1,n) < axis(x2,n);

theorem :: URYSOHN1:22
for n being Nat holds
for x1,x2 being Element of dyadic(n) st x1 < x2 holds
x1 <= (axis(x2,n)-1)/(2|^n) & (axis(x1,n)+1)/(2|^n) <= x2;

theorem :: URYSOHN1:23
for n being Nat holds
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,n+1)+1)/(2|^(n+1)) <= (axis(x2,n+1)-1)/(2|^(n+1));

begin
::
::                             Normal TopSpaces
::

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;
synonym Nbhd of x,T;
end;

theorem :: 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 holds
x in A implies ex B being Nbhd of x,T st B c= A);

canceled;

theorem :: URYSOHN1:26
for T being non empty TopSpace holds
for A being Subset of T holds
(for x being Point of T st x in A holds A is Nbhd of x,T)
implies A is open;

definition
let T be TopStruct;
attr T is being_T1 means
:: URYSOHN1:def 9
for p,q being Point of T st not p = q
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;
synonym T is_T1;
end;

theorem :: URYSOHN1:27
for T being non empty TopSpace holds
T is_T1 iff for p being Point of T holds {p} is closed;

definition
let T be non empty TopSpace;
let F be map of T,R^1;
let x be Point of T;
redefine func F.x -> Real;
end;

theorem :: URYSOHN1:28
for T being non empty TopSpace st T is_T4 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;

theorem :: URYSOHN1:29
for T being non empty TopSpace holds T is_T3 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;

theorem :: URYSOHN1:30
for T being non empty TopSpace st T is_T4 & T is_T1 holds
for A being open Subset of T st A <> {} holds
ex B being Subset of T st B <> {} & Cl(B) c= A;

theorem :: URYSOHN1:31
for T being non empty TopSpace st T is_T4
for A,B being Subset of T st A is open & B is closed & B <> {} & B c= A
ex C being Subset of T st C is open & B c= C & Cl(C) c= A;

begin
::
::              Some increasing family of sets in normal space
::

definition
let T be non empty TopSpace;
let A,B be Subset of T;
assume
T is_T4 & A <> {} & A is open & B is open & Cl(A) c= B;
mode Between of A,B -> Subset of T means
:: URYSOHN1:def 10
it <> {} & it is open & Cl(A) c= it & Cl(it) c= B;
end;

theorem :: URYSOHN1:32
for T being non empty TopSpace st T is_T4
for A,B being closed Subset of T st A <> {} & A misses B
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
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);
```