Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users

### The Urysohn Lemma

by
Jozef Bialas, and
Yatsuka Nakamura

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

```environ

vocabulary ARYTM, COMPTS_1, PRE_TOPC, BOOLE, FUNCT_1, URYSOHN1, SUBSET_1,
ARYTM_1, ARYTM_3, GROUP_1, PARTFUN1, SEQFUNC, RELAT_1, PRALG_2, SUPINF_1,
RCOMP_1, TOPMETR, ORDINAL2, RLVECT_1, TMAP_1, METRIC_1, PCOMPS_1,
ABSVALUE, URYSOHN3;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1,
NAT_1, RELAT_1, FUNCT_1, FUNCT_2, NEWTON, TOPMETR, COMPTS_1, STRUCT_0,
PRE_TOPC, TMAP_1, METRIC_1, PCOMPS_1, SEQFUNC, PARTFUN1, SUPINF_1,
SUPINF_2, MEASURE5, URYSOHN1, ABSVALUE;
constructors TMAP_1, PARTFUN1, SUPINF_2, MEASURE5, URYSOHN1, SEQFUNC, NAT_1,
REAL_1, DOMAIN_1, COMPTS_1, ABSVALUE, WAYBEL_3, MEMBERED;
clusters SUBSET_1, PRE_TOPC, TOPMETR, METRIC_1, SUPINF_1, URYSOHN1, RELSET_1,
XREAL_0, NAT_1, PARTFUN1, STRUCT_0, WAYBEL_3, MEMBERED, ZFMISC_1,
NUMBERS, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;

begin

definition let D be non empty Subset of REAL;
cluster -> real Element of D;
end;

theorem :: URYSOHN3:1
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
(A <> {} & A misses B) holds
for n being Nat holds
ex 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));

definition
let T be non empty TopSpace;
let A,B be Subset of T;
let n be Nat;
assume
T is_T4 & A <> {} & A is closed & B is closed & A misses B;
mode Drizzle of A,B,n -> Function of dyadic(n),bool the carrier of T means
:: URYSOHN3:def 1
A c= it.0 & B = [#]T \ it.1 &
for r1,r2 being Element of dyadic(n) st r1 < r2 holds
(it.r1 is open & it.r2 is open & Cl(it.r1) c= it.r2);
end;

canceled;

theorem :: URYSOHN3:3
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
A <> {} & A misses B holds
for n being Nat,
G being Drizzle of A,B,n holds
ex F being Drizzle of A,B,n+1 st
for r being Element of dyadic(n+1) st
r in dyadic(n) holds F.r = G.r;

definition
let A,B be non empty set;
let F be Function of NAT,PFuncs(A,B);
let n be Nat;
redefine func F.n -> PartFunc of A,B;
end;

theorem :: URYSOHN3:4
for T being non empty TopSpace,
A,B being Subset of T,
n being Nat,
S being Drizzle of A,B,n holds
S is Element of PFuncs(DYADIC,bool the carrier of T);

definition
let A,B be non empty set;
let F be Function of NAT,PFuncs(A,B);
let n be Nat;
redefine func F.n -> Element of PFuncs(A,B);
end;

theorem :: URYSOHN3:5
for T being non empty being_T4 TopSpace holds
for A,B being closed Subset of T st
(A <> {} & A misses B) holds
ex F being Functional_Sequence of DYADIC,bool the carrier of T st
for n being Nat holds
((F.n is Drizzle of A,B,n) &
(for r being Element of dom (F.n) holds (F.n).r = (F.(n+1)).r));

definition
let T be non empty TopSpace;
let A,B be Subset of T;
assume
T is_T4 & A <> {} & A is closed & B is closed & A misses B;
mode Rain of A,B -> Functional_Sequence of DYADIC,bool the carrier of T
means
:: URYSOHN3:def 2
for n being Nat holds
(it.n is Drizzle of A,B,n &
(for r being Element of dom (it.n) holds (it.n).r = (it.(n+1)).r));
end;

definition
let x be Real;
assume
:: URYSOHN3:def 3
((x in dyadic(0) iff it = 0) &
(for n being Nat st (x in dyadic(n+1) & not x in dyadic(n))
holds it = n+1));
end;

theorem :: URYSOHN3:6

theorem :: URYSOHN3:7
for x being Real st x in DYADIC holds
for n being Nat st inf_number_dyadic(x) <= n holds

theorem :: URYSOHN3:8
for x being Real,
n being Nat st x in dyadic(n) holds

theorem :: URYSOHN3:9
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
(A <> {} & A misses B) holds
for G being Rain of A,B,
x being Real st x in DYADIC holds
for n being Nat holds

theorem :: URYSOHN3:10
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
(A <> {} & A misses B) holds
for G being Rain of A,B,
x being Real st x in DYADIC holds
ex y being Element of bool the carrier of T st
(for n being Nat st x in dyadic(n) holds y = (G.n).x);

theorem :: URYSOHN3:11
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
(A <> {} & A misses B) holds
for G being Rain of A,B holds
ex F being Function of DOM,bool the carrier of T st
for x being Real st x in DOM holds
((x in R<0 implies F.x = {}) &
(x in R>1 implies F.x = the carrier of T) &
(for n being Nat st x in dyadic(n) holds F.x = (G.n).x)));

definition
let T be non empty TopSpace;
let A,B be Subset of T;
assume
T is_T4 & A <> {} & A is closed & B is closed & A misses B;
let R be Rain of A,B;
func Tempest(R) -> Function of DOM,bool the carrier of T means
:: URYSOHN3:def 4
for x being Real st x in DOM holds
((x in R<0 implies it.x = {}) &
(x in R>1 implies it.x = the carrier of T) &
(for n being Nat st x in dyadic(n) holds it.x = (R.n).x)));
end;

definition
let X be non empty set;
let T be TopSpace;
let F be Function of X,bool the carrier of T;
let x be Element of X;
redefine func F.x -> Subset of T;
end;

theorem :: URYSOHN3:12
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
A <> {} & A misses B holds
for G being Rain of A,B,
r being Real,
C being Subset of T st C = (Tempest(G)).r &
r in DOM holds
C is open;

theorem :: URYSOHN3:13
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
A <> {} & A misses B holds
for G being Rain of A,B holds
for r1,r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds
for C being Subset of T st C = (Tempest(G)).r1 holds
Cl C c= (Tempest(G)).r2;

theorem :: URYSOHN3:14
for T being non empty TopSpace,
A,B being Subset of T,
G being Rain of A,B,
p being Point of T
ex R being Subset of ExtREAL st
for x being set holds x in R iff (x in DYADIC &
for s being Real st s = x holds not p in (Tempest(G)).s);

definition
let T be non empty TopSpace,
A,B be Subset of T,
R be Rain of A,B,
p be Point of T;
func Rainbow(p,R) -> Subset of ExtREAL means
:: URYSOHN3:def 5
for x being set holds x in it iff (x in DYADIC &
for s being Real st s = x holds not p in (Tempest(R)).s);
end;

definition
let T,S be non empty TopSpace,
F be Function of the carrier of T,the carrier of S,
p be Point of T;
redefine func F.p -> Point of S;
end;

theorem :: URYSOHN3:15
for T being non empty TopSpace,
A,B being Subset of T,
G being Rain of A,B,
p being Point of T holds

theorem :: URYSOHN3:16
for T being non empty TopSpace,
A,B being Subset of T,
R being Rain of A,B
ex F being map of T,R^1 st
for p being Point of T holds
(Rainbow(p,R) = {} implies F.p = 0) &
(for S being non empty Subset of ExtREAL st S = Rainbow(p,R) holds
F.p = sup S);

definition
let T be non empty TopSpace;
let A,B be Subset of T;
let R be Rain of A,B;
func Thunder(R) -> map of T,R^1 means
:: URYSOHN3:def 6
for p being Point of T holds
((Rainbow(p,R) = {} implies it.p = 0) &
(for S being non empty Subset of ExtREAL st S = Rainbow(p,R) holds
it.p = sup S));
end;

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

theorem :: URYSOHN3:17
for T being non empty TopSpace,
A,B being Subset of T,
G being Rain of A,B,
p being Point of T,
S being non empty Subset of ExtREAL st S = Rainbow(p,G) holds
for 1_ being R_eal st 1_ = 1 holds
0. <=' sup S & sup S <=' 1_;

theorem :: URYSOHN3:18
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
(A <> {} & A misses B) holds
for G being Rain of A,B,
r being Element of DOM,
p being Point of T st (Thunder(G)).p < r holds
p in (Tempest(G)).r;

theorem :: URYSOHN3:19
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
(A <> {} & A misses B) holds
for G being Rain of A,B holds
for r being Real st r in DYADIC \/ R>1 & 0 < r holds
for p being Point of T holds
p in (Tempest(G)).r implies (Thunder(G)).p <= r;

theorem :: URYSOHN3:20
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
A <> {} & A misses B holds
for G being Rain of A,B,
n being Nat,
r1 being Element of DOM st 0 < r1 holds
for p being Point of T st r1 < (Thunder(G)).p holds
not p in (Tempest(G)).r1;

theorem :: URYSOHN3:21
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B holds
Thunder(G) is continuous &
(for x being Point of T holds
0 <= (Thunder(G)).x & (Thunder(G)).x <= 1 &
(x in A implies (Thunder(G)).x = 0) &
(x in B implies (Thunder(G)).x = 1));

theorem :: URYSOHN3:22
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
(A <> {} & A misses B) holds
ex F being map of T,R^1 st
F is continuous &
(for x being Point of T holds
0 <= F.x & F.x <= 1 & (x in A implies F.x = 0) & (x in B implies F.x = 1));

::                           Urysohn Lemma

theorem :: URYSOHN3:23
for T being non empty being_T4 TopSpace,
A,B being closed Subset of T st
A misses B holds
ex F being map of T,R^1 st
F is continuous &
(for x being Point of T holds
0 <= F.x & F.x <= 1 & (x in A implies F.x = 0) & (x in B implies F.x = 1));

theorem :: URYSOHN3:24
for T being non empty being_T2 compact TopSpace,
A,B being closed Subset of T st A misses B
ex F being map of T,R^1 st
F is continuous &
(for x being Point of T holds
0 <= F.x & F.x <= 1 & (x in A implies F.x = 0) & (x in B implies F.x = 1));

::  B i b l i o g r a p h y

::  N.Bourbaki, "Topologie Generale", Hermann, Paris 1966.
::  J.Dieudonne, "Foundations of Modern Analysis",Academic Press, 1960.
::  J.L.Kelley, "General Topology", von Nostnend, 1955.
::  K.Yosida, "Functional Analysis", Springer Verlag, 1968.

```