The abstract of the Mizar article:

The Urysohn Lemma

by

Jozef Bialas, and

Yatsuka Nakamura

Received February 16, 2001

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
x in DYADIC;
   func inf_number_dyadic(x) -> Nat means
:: 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
   for x being Real st x in DYADIC holds x in dyadic(inf_number_dyadic(x));

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

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

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
   (G.inf_number_dyadic(x)).x = (G.(inf_number_dyadic(x) + n)).x;

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) &
   (x in DYADIC implies
   (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) &
        (x in DYADIC implies
        (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
   Rainbow(p,G) c= DYADIC;

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.