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