:: Urysohn Lemma :: by J\'ozef Bia{\l}as and Yatsuka Nakamura :: :: Received February 16, 2001 :: Copyright (c) 2001-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, PRE_TOPC, RCOMP_1, SUBSET_1, FUNCT_1, URYSOHN1, CARD_1, ZFMISC_1, STRUCT_0, TARSKI, ARYTM_3, PARTFUN1, SEQFUNC, RELAT_1, NEWTON, XXREAL_0, NAT_1, ARYTM_1, REAL_1, CARD_3, PROB_1, LIMFUNC1, SUPINF_1, TOPMETR, ORDINAL2, XXREAL_1, SUPINF_2, XXREAL_2, TMAP_1, METRIC_1, PCOMPS_1, COMPLEX1, URYSOHN3; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_1, XXREAL_2, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, NEWTON, SUPINF_2, TOPMETR, STRUCT_0, PRE_TOPC, COMPTS_1, TMAP_1, METRIC_1, PCOMPS_1, SEQFUNC, PROB_1, LIMFUNC1, SUPINF_1, URYSOHN1; constructors REAL_1, PROB_1, LIMFUNC1, NEWTON, SUPINF_2, MEASURE5, URYSOHN1, TMAP_1, WAYBEL_3, PCOMPS_1, BORSUK_6, COMPTS_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, NUMBERS, XXREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, URYSOHN1, TOPMETR, WAYBEL_3, VALUED_0, XREAL_0, FUNCT_1, NEWTON; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin theorem :: URYSOHN3:1 for T being non empty normal 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 normal & 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; theorem :: URYSOHN3:2 for T being non empty normal 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; theorem :: URYSOHN3:3 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); theorem :: URYSOHN3:4 for T being non empty normal TopSpace, 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 normal & 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:5 for x being Real st x in DYADIC holds x in dyadic( inf_number_dyadic(x)); theorem :: URYSOHN3:6 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:7 for x being Real, n being Nat st x in dyadic(n) holds inf_number_dyadic(x) <= n; theorem :: URYSOHN3:8 for T being non empty normal 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:9 for T being non empty normal 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 Subset of T st for n being Nat st x in dyadic(n) holds y = (G.n).x; theorem :: URYSOHN3:10 for T being non empty normal 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 halfline 0 implies F.x = {}) & (x in right_open_halfline 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 normal & 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 halfline 0 implies it.x = {}) & (x in right_open_halfline 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; theorem :: URYSOHN3:11 for T being non empty normal 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:12 for T being non empty normal 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; definition let T be non empty TopSpace, A,B be Subset of T, G be Rain of A,B, p be Point of T; func Rainbow(p,G) -> 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 G).s ); end; theorem :: URYSOHN3:13 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; definition let T be non empty TopSpace; let A,B be Subset of T; let R be Rain of A,B; func Thunder(R) -> Function 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; 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, S being non empty Subset of ExtREAL st S = Rainbow(p,G) holds for e1 being R_eal st e1 = 1 holds 0. <= sup S & sup S <= e1 ; theorem :: URYSOHN3:15 for T being non empty normal 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:16 for T being non empty normal 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 \/ (right_open_halfline 1) & 0 < r holds for p being Point of T holds p in (Tempest G).r implies (Thunder G).p <= r; theorem :: URYSOHN3:17 for T being non empty normal TopSpace, A,B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A,B, 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:18 for T being non empty normal 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:19 for T being non empty normal TopSpace, A,B being closed Subset of T st A <> {} & A misses B holds ex F being Function 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); ::$N Urysohn's lemma theorem :: URYSOHN3:20 for T being non empty normal TopSpace, A,B being closed Subset of T st A misses B holds ex F being Function 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:21 for T being non empty T_2 compact TopSpace, A,B being closed Subset of T st A misses B ex F being Function 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.