Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### 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.

Back to top