:: Urysohn Lemma
:: by J\'ozef Bia{\l}as and Yatsuka Nakamura
::
:: Received February 16, 2001
:: Copyright (c) 2001-2026 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;
definitions PRE_TOPC, TARSKI;
equalities STRUCT_0, LIMFUNC1, PROB_1;
expansions PRE_TOPC, TARSKI;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, PCOMPS_1, PRE_TOPC, TOPS_1, TOPMETR,
ABSVALUE, PARTFUN1, URYSOHN1, XREAL_0, RELSET_1, URYSOHN2, TMAP_1,
METRIC_1, XBOOLE_0, XBOOLE_1, PREPOWER, XCMPLX_1, XREAL_1, PEPIN, NEWTON,
XXREAL_0, SUBSET_1, NUMBERS, XXREAL_1, XXREAL_2, RELAT_1;
schemes NAT_1, FUNCT_2, RECDEF_1, XBOOLE_0;
begin
Lm1: for T being non empty normal TopSpace, A,B being closed Subset of T st A
<> {} & A misses B ex G being Function of dyadic(0),bool the carrier of T st A
c= G.0 & B = [#]T \ G.1 & for r1,r2 being Element of dyadic(0) st r1 < r2 holds
G.r1 is open & G.r2 is open & Cl(G.r1) c= G.r2
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume that
A1: A <> {} and
A2: A misses B;
reconsider G1 = [#]T \ B as Subset of T;
A3: G1 = B` by SUBSET_1:def 4;
then
A4: G1 is open by TOPS_1:3;
A \ B c= G1 by XBOOLE_1:33;
then A c= G1 by A2,XBOOLE_1:83;
then consider G0 being Subset of T such that
A5: G0 is open and
A6: A c= G0 and
A7: Cl(G0) c= G1 by A1,A4,URYSOHN1:23;
defpred P[set,set] means ($1 = 0 implies $2 = G0) & ($1 = 1 implies $2 = G1);
A8: for x being Element of dyadic(0) ex y being Subset of T st P[x,y]
proof
let x be Element of dyadic(0);
per cases by TARSKI:def 2,URYSOHN1:2;
suppose
A9: x = 0;
take G0;
thus thesis by A9;
end;
suppose
A10: x = 1;
take G1;
thus thesis by A10;
end;
end;
ex F being Function of dyadic(0),bool the carrier of T st for x being
Element of dyadic(0) holds P[x,F.x] from FUNCT_2:sch 3(A8);
then consider F being Function of dyadic(0),bool the carrier of T such that
A11: for x being Element of dyadic(0) holds P[x,F.x];
A12: for r1,r2 being Element of dyadic(0) st r1 < r2 holds F.r1 is open & F.
r2 is open & Cl(F.r1) c= F.r2
proof
let r1,r2 be Element of dyadic(0);
A13: r1 = 0 or r1 = 1 by TARSKI:def 2,URYSOHN1:2;
A14: r2 = 0 or r2 = 1 by TARSKI:def 2,URYSOHN1:2;
assume
A15: r1 < r2;
then F.1 = G1 by A11,A14,URYSOHN1:2;
hence thesis by A3,A5,A7,A11,A15,A13,A14,TOPS_1:3;
end;
take F;
1 in dyadic(0) by TARSKI:def 2,URYSOHN1:2;
then 0 in dyadic(0) & F.1 = G1 by A11,TARSKI:def 2,URYSOHN1:2;
hence thesis by A6,A11,A12,PRE_TOPC:3;
end;
theorem Th1:
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
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume that
A1: A <> {} and
A2: A misses B;
defpred P[Nat] means
ex G being Function of dyadic($1),bool the
carrier of T st A c= G.0 & B = [#]T \ G.1 & (for r1,r2 being Element of dyadic(
$1) st r1 < r2 holds (G.r1 is open & G.r2 is open & Cl(G.r1) c= G.r2));
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
given G being Function of dyadic(n),bool the carrier of T such that
A4: 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;
consider F being Function of dyadic(n+1),bool the carrier of T such that
A5: A c= F.0 & B = [#]T \ F.1 & for r1,r2,r being Element of dyadic(n+
1) st r1 < r2 holds F.r1 is open & F.r2 is open & Cl(F.r1) c= F.r2 & (r in
dyadic(n) implies F.r = G.r) by A1,A4,URYSOHN1:24;
take F;
thus thesis by A5;
end;
A6: P[0] by A1,A2,Lm1;
thus for n being Nat holds P[n] from NAT_1:sch 2(A6,A3);
end;
definition
let T be non empty TopSpace;
let A,B be Subset of T;
let n be Nat;
assume
A1: 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
:
Def1: 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;
existence by A1,Th1;
end;
theorem Th2:
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
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume that
A1: A <> {} and
A2: A misses B;
let n be Nat;
let G be Drizzle of A,B,n;
A3: 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 by A1,A2,Def1;
A c= G.0 & B = [#]T \ G.1 by A1,A2,Def1;
then consider
F being Function of dyadic(n+1),bool the carrier of T such that
A4: A c= F.0 & B = [#]T \ F.1 and
A5: for r1,r2,r being Element of dyadic(n+1) st r1 < r2 holds F.r1 is
open & F.r2 is open & Cl(F.r1) c= F.r2 & (r in dyadic(n) implies F.r = G.r) by
A1,A3,URYSOHN1:24;
for r1,r2 being Element of dyadic(n+1) st r1 < r2 holds F.r1 is open & F
.r2 is open & Cl(F.r1) c= F.r2 by A5;
then reconsider F as Drizzle of A,B,n+1 by A1,A2,A4,Def1;
take F;
let r be Element of dyadic(n+1);
A6: 0 in dyadic(n+1) & 1 in dyadic(n+1) by URYSOHN1:6;
assume r in dyadic(n);
hence thesis by A5,A6;
end;
theorem Th3:
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)
proof
let T be non empty TopSpace;
let A,B be Subset of T;
let n be Nat;
let S be Drizzle of A,B,n;
dyadic(n) c= DYADIC by URYSOHN2:23;
then S is PartFunc of DYADIC,bool the carrier of T by RELSET_1:7;
hence thesis by PARTFUN1:45;
end;
theorem Th4:
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
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
defpred P[object] means ex n being Nat st $1 is Drizzle of A,B,n;
consider D being set such that
A1: for x being object holds x in D iff x in PFuncs(DYADIC,bool the carrier
of T) & P[x] from XBOOLE_0:sch 1;
set S = the Drizzle of A,B,0;
A2: S is Element of PFuncs(DYADIC,bool the carrier of T) by Th3;
then reconsider D as non empty set by A1;
reconsider S as Element of D by A1,A2;
defpred P1[Element of D,Element of D] means ex xx,yy being PartFunc of
DYADIC,bool the carrier of T st (xx=$1 & yy = $2 & (ex k being Nat
st xx is Drizzle of A,B,k) & (for k being Nat st xx is Drizzle of A,
B,k holds yy is Drizzle of A,B,k+1) & (for r being Element of dom xx holds xx.r
= yy.r));
defpred Q[Nat,Element of D,Element of D] means P1[$2,$3];
assume
A3: A <> {} & A misses B;
A4: for n being Nat for x being Element of D ex y being Element
of D st Q[n,x,y]
proof
let n be Nat;
let x be Element of D;
consider s0 being Nat such that
A5: x is Drizzle of A,B,s0 by A1;
reconsider xx = x as Drizzle of A,B,s0 by A5;
consider yy being Drizzle of A,B,s0+1 such that
A6: for r being Element of dyadic(s0+1) holds (r in dyadic(s0) implies
yy.r = xx.r) by A3,Th2;
A7: for r being Element of dom xx holds xx.r = yy.r
proof
let r be Element of dom xx;
dom xx = dyadic(s0) by FUNCT_2:def 1;
then
A8: r in dyadic(s0);
dyadic(s0) c= dyadic(s0+1) by URYSOHN1:5;
hence thesis by A6,A8;
end;
A9: for k being Nat st xx is Drizzle of A,B,k holds yy is
Drizzle of A,B,k+1
proof
let k be Nat;
assume xx is Drizzle of A,B,k;
then
A10: dom xx = dyadic(k) by FUNCT_2:def 1;
k = s0
proof
assume
A11: k <> s0;
per cases by A11,XXREAL_0:1;
suppose
A12: k < s0;
set o = 1/(2|^s0);
A13: not o in dyadic(k)
proof
A14: (2|^k) < 1 * (2|^s0) by A12,PEPIN:66;
assume o in dyadic(k);
then consider i being Nat such that
i <= (2|^k) and
A15: o = i/(2|^k) by URYSOHN1:def 1;
A16: 0 < 2|^s0 by NEWTON:83;
0 < 2|^k by NEWTON:83;
then
A17: 1*(2|^k) = i*(2|^s0) by A15,A16,XCMPLX_1:95;
then
A18: i = (2|^k)/(2|^s0) by A16,XCMPLX_1:89;
A19: not ex n being Nat st i = n + 1
proof
given n being Nat such that
A20: i = n + 1;
n + 1 -1 < 0 by A18,A14,A20,XREAL_1:49,83;
hence thesis;
end;
i <> 0 by A17,NEWTON:83;
hence thesis by A19,NAT_1:6;
end;
1 <= (2|^s0) by PREPOWER:11;
then o in dyadic(s0) by URYSOHN1:def 1;
hence thesis by A10,A13,FUNCT_2:def 1;
end;
suppose
A21: s0 < k;
set o = 1/(2|^k);
A22: not o in dyadic(s0)
proof
A23: (2|^s0) < 1 * (2|^k) by A21,PEPIN:66;
assume o in dyadic(s0);
then consider i being Nat such that
i <= (2|^s0) and
A24: o = i/(2|^s0) by URYSOHN1:def 1;
A25: 0 < 2|^k by NEWTON:83;
0 < 2|^s0 by NEWTON:83;
then
A26: 1*(2|^s0) = i*(2|^k) by A24,A25,XCMPLX_1:95;
then
A27: i = (2|^s0)/(2|^k) by A25,XCMPLX_1:89;
A28: not ex n being Nat st i = n + 1
proof
given n being Nat such that
A29: i = n + 1;
n + 1 -1 < 0 by A27,A23,A29,XREAL_1:49,83;
hence thesis;
end;
i <> 0 by A26,NEWTON:83;
hence thesis by A28,NAT_1:6;
end;
1 <= (2|^k) by PREPOWER:11;
then o in dyadic(k) by URYSOHN1:def 1;
hence thesis by A10,A22,FUNCT_2:def 1;
end;
end;
hence thesis;
end;
reconsider xx as Element of PFuncs(DYADIC,bool the carrier of T) by Th3;
reconsider xx as Element of D;
A30: yy is Element of PFuncs(DYADIC,bool the carrier of T) by Th3;
then reconsider yy as Element of D by A1;
ex y being Element of D st P1[x,y]
proof
take yy;
reconsider yy as PartFunc of DYADIC, bool the carrier of T by A30,
PARTFUN1:46;
reconsider xx as PartFunc of DYADIC, bool the carrier of T by PARTFUN1:47
;
take xx,yy;
thus thesis by A9,A7;
end;
then consider y being Element of D such that
A31: P1[x,y];
take y;
thus thesis by A31;
end;
ex F being sequence of D st F.0 = S & for n being Nat
holds Q[n,F.n,F.(n+1)] from RECDEF_1:sch 2(A4);
then consider F being sequence of D such that
A32: F.0 = S and
A33: for n being Nat holds P1[F.n,F.(n+1)];
for x being object holds x in D implies x in PFuncs(DYADIC,bool the
carrier of T) by A1;
then rng F c= D & D c= PFuncs(DYADIC,bool the carrier of T) by RELAT_1:def 19
;
then
A34: dom F = NAT & rng F c= PFuncs(DYADIC,bool the carrier of T) by
FUNCT_2:def 1;
defpred R[Nat,PartFunc of DYADIC,bool the carrier of T,
PartFunc
of DYADIC,bool the carrier of T] means ($2=F.$1 & $3 = F.($1+1) & (ex k being
Nat st $2 is Drizzle of A,B,k) & (for k being Nat st $2
is Drizzle of A,B,k holds $3 is Drizzle of A,B,k+1) & (for r being Element of
dom $2 holds $2.r = $3.r));
reconsider F as Functional_Sequence of DYADIC,bool the carrier of T by A34,
FUNCT_2:def 1,RELSET_1:4;
defpred P[Nat] means F.$1 is Drizzle of A,B,$1 &
for r being Element of dom (F.$1) holds (F.$1).r = (F.($1+1)).r;
A35: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A36: P[n];
ex xx,yy being PartFunc of DYADIC,bool the carrier of T st R[n,xx,yy]
by A33;
hence F.(n+1) is Drizzle of A,B,(n+1) by A36;
let r be Element of dom (F.(n+1));
ex xx1,yy1 being PartFunc of DYADIC,bool the carrier of T st R[n+1,xx1
,yy1] by A33;
hence thesis;
end;
take F;
ex xx,yy being PartFunc of DYADIC,bool the carrier of T st R[0,xx,yy] by A33;
then
A37: P[0] by A32;
for n being Nat holds P[n] from NAT_1:sch 2(A37,A35);
hence thesis;
end;
definition
let T be non empty TopSpace;
let A,B be Subset of T;
assume
A1: 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
:Def2:
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;
existence by A1,Th4;
end;
definition
let x be Real;
assume
A1: x in DYADIC;
func inf_number_dyadic(x) -> Nat means
:Def3:
(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;
existence
proof
defpred P[Nat] means x in dyadic($1);
ex s being Nat st P[s] by A1,URYSOHN1:def 2;
then
A2: ex s being Nat st P[s];
ex q being Nat st P[q] & for i being Nat st P[i] holds q <= i from
NAT_1:sch 5(A2);
then consider q being Nat such that
A3: x in dyadic(q) and
A4: for i being Nat st x in dyadic(i) holds q <= i;
reconsider q as Nat;
take q;
for n being Nat st x in dyadic(n+1) & not x in dyadic(n)
holds q = n+1
proof
let n be Nat;
assume that
A5: x in dyadic(n+1) and
A6: not x in dyadic(n);
A7: n + 1 <= q
proof
assume not n + 1 <= q;
then q <= n by NAT_1:13;
then dyadic(q) c= dyadic(n) by URYSOHN2:29;
hence thesis by A3,A6;
end;
q <= n + 1 by A4,A5;
hence thesis by A7,XXREAL_0:1;
end;
hence thesis by A3,A4;
end;
uniqueness
proof
let s1,s2 be Nat such that
A8: x in dyadic(0) iff s1 = 0 and
A9: for n being Nat st x in dyadic(n+1) & not x in dyadic(
n ) holds s1 = n+1 and
A10: x in dyadic(0) iff s2 = 0 and
A11: for n being Nat st x in dyadic(n+1) & not x in dyadic(
n ) holds s2 = n+1;
per cases;
suppose
s1 = 0;
hence thesis by A8,A10;
end;
suppose
A12: 0 < s1;
defpred P[Nat] means x in dyadic($1);
ex s being Nat st P[s] by A1,URYSOHN1:def 2;
then
A13: ex s being Nat st P[s];
ex q being Nat st P[q] & for i being Nat st P[i] holds q <= i from
NAT_1:sch 5(A13);
then consider q being Nat such that
A14: x in dyadic(q) and
A15: for i being Nat st x in dyadic(i) holds q <= i;
now
per cases;
case
q = 0;
hence thesis by A8,A12,A14;
end;
case
0 < q;
then consider m being Nat such that
A16: q = m + 1 by NAT_1:6;
reconsider m as Nat;
A17: not x in dyadic(m)
proof
assume x in dyadic(m);
then m + 1 <= m + 0 by A15,A16;
hence thesis by XREAL_1:6;
end;
then s1 = m + 1 by A9,A14,A16;
hence thesis by A11,A14,A16,A17;
end;
end;
hence thesis;
end;
end;
end;
theorem Th5:
for x being Real st x in DYADIC holds x in dyadic( inf_number_dyadic(x))
proof
let x be Real;
set s = inf_number_dyadic(x);
defpred P[Nat] means not x in dyadic(s + 1 + $1);
assume
A1: x in DYADIC;
then consider k being Nat such that
A2: x in dyadic(k) by URYSOHN1:def 2;
A3: for i being Nat st P[i] holds P[(i+1)]
proof
let i be Nat;
assume
A4: not x in dyadic(s + 1 + i);
assume x in dyadic(s + 1 + (i + 1));
then x in dyadic(s + 1 + i + 1);
then s + 0 = s + (i + 2) by A1,A4,Def3;
hence thesis;
end;
assume
A5: not x in dyadic(s);
A6: s < k
proof
assume not s < k;
then dyadic(k) c= dyadic(s) by URYSOHN2:29;
hence thesis by A5,A2;
end;
then consider i being Nat such that
A7: k = i + 1 by NAT_1:6;
s <= i by A6,A7,NAT_1:13;
then consider m being Nat such that
A8: i = s + m by NAT_1:10;
reconsider m as Nat;
A9: P[0] by A1,A5,Def3;
for i being Nat holds P[i] from NAT_1:sch 2(A9,A3);
then not x in dyadic(s + 1 + m);
hence thesis by A2,A7,A8;
end;
theorem Th6:
for x being Real st x in DYADIC holds for n being Nat
st inf_number_dyadic(x) <= n holds x in dyadic(n)
proof
let x be Real;
assume x in DYADIC;
then
A1: x in dyadic(inf_number_dyadic(x)) by Th5;
let n be Nat;
assume inf_number_dyadic(x) <= n;
then dyadic(inf_number_dyadic(x)) c= dyadic(n) by URYSOHN2:29;
hence thesis by A1;
end;
theorem Th7:
for x being Real, n being Nat st x in dyadic(n) holds
inf_number_dyadic(x) <= n
proof
let x be Real;
let n be Nat;
A1: dyadic n c= DYADIC by URYSOHN2:23;
defpred P[Nat] means x in dyadic($1);
assume
A2: x in dyadic(n);
then
A3: ex s being Nat st P[s];
ex q being Nat st P[q] & for i being Nat st P[i] holds q <= i from NAT_1
:sch 5(A3);
then consider q being Nat such that
A4: x in dyadic(q) and
A5: for i being Nat st x in dyadic(i) holds q <= i;
A6: q <= n by A2,A5;
now
per cases;
case
q = 0;
hence thesis by A2,A1,A4,Def3;
end;
case
0 < q;
then consider m being Nat such that
A7: q = m + 1 by NAT_1:6;
reconsider m as Nat;
not x in dyadic(m)
proof
assume x in dyadic(m);
then m + 1 <= m + 0 by A5,A7;
hence thesis by XREAL_1:6;
end;
hence thesis by A2,A1,A4,A6,A7,Def3;
end;
end;
hence thesis;
end;
theorem Th8:
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
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A1: A <> {} & A misses B;
let G be Rain of A,B;
let x be Real;
set s = inf_number_dyadic(x);
defpred Q[Nat] means (G.s).x = (G.(s + $1)).x;
assume
A2: x in DYADIC;
A3: for n being Nat st Q[n] holds Q[(n+1)]
proof
let n be Nat;
assume
A4: (G.s).x = (G.(s + n)).x;
s <= s + (n + 1) by NAT_1:11;
then
A5: x in dyadic(s + n + 1) by A2,Th6;
G.(s + n) is Drizzle of A,B,s + n by A1,Def2;
then
A6: dom(G.(s + n)) = dyadic(s + n) by FUNCT_2:def 1;
x in dyadic(s + n) by A2,Th6,NAT_1:11;
hence thesis by A1,A4,A5,A6,Def2;
end;
A7: Q[0];
for i be Nat holds Q[i] from NAT_1:sch 2(A7,A3);
hence thesis;
end;
theorem Th9:
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
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A1: A <> {} & A misses B;
let G be Rain of A,B;
let x be Real;
assume
A2: x in DYADIC;
reconsider s = inf_number_dyadic(x) as Nat;
G.s is Drizzle of A,B,s by A1,Def2;
then reconsider y = (G.s).x as Subset of T by A2,Th5,FUNCT_2:5;
take y;
let n be Nat;
assume x in dyadic(n);
then consider m being Nat such that
A3: n = s + m by Th7,NAT_1:10;
thus thesis by A1,A2,A3,Th8;
end;
theorem Th10:
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 )
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A1: A <> {} & A misses B;
let G be Rain of A,B;
defpred P[Element of DOM,set] means (($1 in halfline 0 implies $2 = {}) & (
$1 in right_open_halfline 1 implies $2 = the carrier of T) & ($1 in DYADIC
implies (for n being Nat st $1 in dyadic(n) holds $2 = (G.n).$1)));
A2: for x being Element of DOM ex y being Subset of T st P[x,y]
proof
reconsider a = 0, b = 1 as R_eal by XXREAL_0:def 1;
let x be Element of DOM;
A3: x in halfline 0 \/ DYADIC or x in right_open_halfline 1 by URYSOHN1:def 3
,XBOOLE_0:def 3;
per cases by A3,XBOOLE_0:def 3;
suppose
A4: x in halfline 0;
A5: not x in right_open_halfline 1 & not x in DYADIC
proof
assume
A6: x in right_open_halfline 1 or x in DYADIC;
per cases by A6;
suppose
x in right_open_halfline 1;
then 1 < x by XXREAL_1:235;
hence thesis by A4,XXREAL_1:233;
end;
suppose
A7: x in DYADIC;
reconsider x as R_eal by XXREAL_0:def 1;
a <= x by A7,URYSOHN2:28,XXREAL_1:1;
hence thesis by A4,XXREAL_1:233;
end;
end;
reconsider s = {} as Subset of T by XBOOLE_1:2;
s = s;
hence thesis by A5;
end;
suppose
A8: x in DYADIC;
A9: not x in halfline 0
proof
assume
A10: x in halfline 0;
reconsider x as R_eal by XXREAL_0:def 1;
a <= x by A8,URYSOHN2:28,XXREAL_1:1;
hence thesis by A10,XXREAL_1:233;
end;
A11: not x in right_open_halfline 1
proof
assume
A12: x in right_open_halfline 1;
reconsider x as R_eal by XXREAL_0:def 1;
x <= b by A8,URYSOHN2:28,XXREAL_1:1;
hence thesis by A12,XXREAL_1:235;
end;
ex s being Subset of T st for n being Nat st x in dyadic(
n) holds s = (G.n).x by A1,A8,Th9;
hence thesis by A11,A9;
end;
suppose
A13: x in right_open_halfline 1;
A14: not x in halfline 0 & not x in DYADIC
proof
assume
A15: x in halfline 0 or x in DYADIC;
per cases by A15;
suppose
x in halfline 0;
then x < 0 by XXREAL_1:233;
hence thesis by A13,XXREAL_1:235;
end;
suppose
A16: x in DYADIC;
reconsider x as R_eal by XXREAL_0:def 1;
x <= b by A16,URYSOHN2:28,XXREAL_1:1;
hence thesis by A13,XXREAL_1:235;
end;
end;
the carrier of T c= the carrier of T;
then reconsider s = the carrier of T as Subset of T;
s = s;
hence thesis by A14;
end;
end;
ex F being Function of DOM,bool the carrier of T st for x being Element
of DOM holds P[x,F.x] from FUNCT_2:sch 3(A2);
then consider F being Function of DOM,bool the carrier of T such that
A17: for x being Element of DOM holds P[x,F.x];
take F;
thus thesis by A17;
end;
definition
let T be non empty TopSpace;
let A,B be Subset of T;
assume
A1: 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
:Def4:
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 );
existence by A1,Th10;
uniqueness
proof
let G1,G2 be Function of DOM,bool the carrier of T such that
A2: for x being Real st x in DOM holds (x in halfline 0 implies G1.x =
{}) & (x in right_open_halfline 1 implies G1.x = the carrier of T) & (x in
DYADIC implies for n being Nat st x in dyadic(n) holds G1.x = (R.n).
x ) and
A3: for x being Real st x in DOM holds (x in halfline 0 implies G2.x =
{}) & (x in right_open_halfline 1 implies G2.x = the carrier of T) & (x in
DYADIC implies for n being Nat st x in dyadic(n) holds G2.x = (R.n).
x );
for x being object st x in DOM holds G1.x = G2.x
proof
let x be object;
assume
A4: x in DOM;
then reconsider x as Real;
A5: x in halfline 0 \/ DYADIC or x in right_open_halfline 1 by A4,
URYSOHN1:def 3,XBOOLE_0:def 3;
per cases by A5,XBOOLE_0:def 3;
suppose
A6: x in halfline 0;
then G1.x = {} by A2,A4;
hence thesis by A3,A4,A6;
end;
suppose
A7: x in right_open_halfline 1;
then G1.x = the carrier of T by A2,A4;
hence thesis by A3,A4,A7;
end;
suppose
A8: x in DYADIC;
then consider n being Nat such that
A9: x in dyadic(n) by URYSOHN1:def 2;
G1.x = (R.n).x by A2,A4,A8,A9;
hence thesis by A3,A4,A8,A9;
end;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th11:
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
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A1: A <> {} & A misses B;
let G be Rain of A,B;
let r be Real;
let C be Subset of T;
assume that
A2: C = (Tempest G).r and
A3: r in DOM;
A4: r in halfline 0 \/ DYADIC or r in right_open_halfline 1 by A3,
URYSOHN1:def 3,XBOOLE_0:def 3;
per cases by A4,XBOOLE_0:def 3;
suppose
r in halfline 0;
then C = {} by A1,A2,A3,Def4;
then C in the topology of T by PRE_TOPC:1;
hence thesis;
end;
suppose
A5: r in DYADIC;
then consider n being Nat such that
A6: r in dyadic(n) by URYSOHN1:def 2;
reconsider D = G.n as Drizzle of A,B,n by A1,Def2;
A7: for r1,r2 being Element of dyadic(n) st r1 < r2 holds D.r1 is open &
D.r2 is open & Cl(D.r1) c= D.r2 & A c= D.0 & B = [#]T \ D.1 by A1,Def1;
A8: (Tempest G).r = (G.n).r by A1,A3,A5,A6,Def4;
now
per cases by A6,URYSOHN1:1;
case
A9: r = 0;
then reconsider r as Element of dyadic(n) by URYSOHN1:6;
1 is Element of dyadic(n) & D.r = C by A1,A2,A3,A5,Def4,URYSOHN1:6;
hence thesis by A1,A9,Def1;
end;
case
A10: 0 < r;
0 in dyadic(n) by URYSOHN1:6;
hence thesis by A2,A6,A8,A7,A10;
end;
end;
hence thesis;
end;
suppose
A11: r in right_open_halfline 1;
A12: the carrier of T in the topology of T by PRE_TOPC:def 1;
C = the carrier of T by A1,A2,A3,A11,Def4;
hence thesis by A12;
end;
end;
theorem Th12:
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
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A1: A <> {} & A misses B;
let G be Rain of A,B;
let r1,r2 be Real;
assume that
A2: r1 in DOM and
A3: r2 in DOM and
A4: r1 < r2;
A5: r1 in halfline 0 \/ DYADIC or r1 in right_open_halfline 1 by A2,
URYSOHN1:def 3,XBOOLE_0:def 3;
A6: r2 in halfline 0 \/ DYADIC or r2 in right_open_halfline 1 by A3,
URYSOHN1:def 3,XBOOLE_0:def 3;
let C be Subset of T;
assume
A7: C = (Tempest G).r1;
per cases by A5,A6,XBOOLE_0:def 3;
suppose
A8: r1 in halfline 0 & r2 in halfline 0;
C = {} by A1,A2,A7,A8,Def4;
then Cl C = {} by PRE_TOPC:22;
hence thesis;
end;
suppose
r1 in DYADIC & r2 in halfline 0;
then r2 < 0 & ex s being Nat st r1 in dyadic(s) by
URYSOHN1:def 2,XXREAL_1:233;
hence thesis by A4,URYSOHN1:1;
end;
suppose
A9: r1 in right_open_halfline 1 & r2 in halfline 0;
then 1 < r1 by XXREAL_1:235;
hence thesis by A4,A9,XXREAL_1:233;
end;
suppose
A10: r1 in halfline 0 & r2 in DYADIC;
C = {} by A1,A2,A7,A10,Def4;
then Cl C = {} by PRE_TOPC:22;
hence thesis;
end;
suppose
A11: r1 in DYADIC & r2 in DYADIC;
then consider n2 being Nat such that
A12: r2 in dyadic(n2) by URYSOHN1:def 2;
consider n1 being Nat such that
A13: r1 in dyadic(n1) by A11,URYSOHN1:def 2;
set n = n1 + n2;
A14: dyadic(n1) c= dyadic(n) by NAT_1:11,URYSOHN2:29;
then
A15: (Tempest G).r1 = (G.n).r1 by A1,A2,A11,A13,Def4;
dyadic(n2) c= dyadic(n) by NAT_1:11,URYSOHN2:29;
then reconsider r1,r2 as Element of dyadic(n) by A13,A12,A14;
reconsider D = G.n as Drizzle of A,B,n by A1,Def2;
Cl(D.r1) c= D.r2 by A1,A4,Def1;
hence thesis by A1,A3,A7,A11,A15,Def4;
end;
suppose
A16: r1 in right_open_halfline 1 & r2 in DYADIC;
then ex s being Nat st r2 in dyadic(s) by URYSOHN1:def 2;
then
A17: r2 <= 1 by URYSOHN1:1;
1 < r1 by A16,XXREAL_1:235;
hence thesis by A4,A17,XXREAL_0:2;
end;
suppose
A18: r1 in halfline 0 & r2 in right_open_halfline 1;
C = {} by A1,A2,A7,A18,Def4;
then Cl C = {} by PRE_TOPC:22;
hence thesis;
end;
suppose
r1 in DYADIC & r2 in right_open_halfline 1;
then (Tempest G).r2 = the carrier of T by A1,A3,Def4;
hence thesis;
end;
suppose
r1 in right_open_halfline 1 & r2 in right_open_halfline 1;
then (Tempest G).r2 = the carrier of T by A1,A3,Def4;
hence thesis;
end;
end;
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
:Def5:
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
);
existence
proof
defpred P[object] means
for s being Real st s = $1 holds not p in (Tempest G).s;
consider R being set such that
A1: for x being object holds x in R iff x in DYADIC & P[x]
from XBOOLE_0:sch 1;
R c= REAL
proof
let x be object;
assume x in R;
then x in DYADIC by A1;
hence thesis;
end;
then reconsider R as Subset of ExtREAL by NUMBERS:31,XBOOLE_1:1;
take R;
thus thesis by A1;
end;
uniqueness
proof
let R1,R2 be Subset of ExtREAL such that
A2: for x being set holds x in R1 iff (x in DYADIC & for s being Real
st s = x holds not p in (Tempest G).s) and
A3: for x being set holds x in R2 iff (x in DYADIC & for s being Real
st s = x holds not p in (Tempest G).s);
for x being object holds x in R1 iff x in R2
proof
let x be object;
hereby
assume x in R1;
then
x in DYADIC & for s being Real st s = x holds not p in (Tempest G)
.s by A2;
hence x in R2 by A3;
end;
assume x in R2;
then
x in DYADIC & for s being Real st s = x holds not p in (Tempest G).s
by A3;
hence thesis by A2;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th13:
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
by Def5;
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
:Def6:
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;
existence
proof
defpred P[Element of T,set] means ((Rainbow($1,R) = {} implies $2 = 0) & (
for S being non empty Subset of ExtREAL st S = Rainbow($1,R) holds $2 = sup S))
;
A1: for x being Element of T ex y being Element of R^1 st P[x,y]
proof
let x be Element of T;
per cases;
suppose
A2: Rainbow(x,R) = {};
0 in REAL by XREAL_0:def 1;
then reconsider y = 0 as Element of R^1 by TOPMETR:17;
P[x,y] by A2;
hence thesis;
end;
suppose
Rainbow(x,R) <> {};
then reconsider S = Rainbow(x,R) as non empty Subset of ExtREAL;
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
consider q being object such that
A3: q in S by XBOOLE_0:def 1;
reconsider q as R_eal by A3;
A4: 0 in REAL by XREAL_0:def 1;
A5: 1 in REAL by XREAL_0:def 1;
S c= DYADIC by Th13;
then S c= [.0.,e1.] by URYSOHN2:28;
then
A6: 0 <= inf S & sup S <= 1 by URYSOHN2:26;
inf S <= q & q <= sup S by A3,XXREAL_2:3,4;
then sup S in REAL by A6,XXREAL_0:45,A4,A5;
then reconsider y = sup S as Element of R^1
by TOPMETR:17;
take y;
thus thesis;
end;
end;
ex F being Function of the carrier of T,the carrier of R^1 st for x
being Element of T holds P[x,F.x] from FUNCT_2:sch 3(A1);
then consider F being Function of T,R^1 such that
A7: for x being Element of T holds P[x,F.x];
take F;
thus thesis by A7;
end;
uniqueness
proof
let G1,G2 be Function of T,R^1 such that
A8: for p being Point of T holds (Rainbow(p,R) = {} implies G1.p = 0)
& for S being non empty Subset of ExtREAL st S = Rainbow(p,R) holds G1.p = sup
S and
A9: for p being Point of T holds (Rainbow(p,R) = {} implies G2.p = 0)
& for S being non empty Subset of ExtREAL st S = Rainbow(p,R) holds G2.p = sup
S;
for x being object st x in the carrier of T holds G1.x = G2.x
proof
let x be object;
assume x in the carrier of T;
then reconsider x as Point of T;
per cases;
suppose
A10: Rainbow(x,R) = {};
then G1.x = 0 by A8
.= G2.x by A9,A10;
hence thesis;
end;
suppose
Rainbow(x,R) <> {};
then reconsider S = Rainbow(x,R) as non empty Subset of ExtREAL;
G1.x = sup S by A8
.= G2.x by A9;
hence thesis;
end;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th14:
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
proof
reconsider a = 0,b = 1 as R_eal by XXREAL_0:def 1;
let T be non empty TopSpace, A,B be Subset of T, G be Rain of A,B, p be
Point of T, S be non empty Subset of ExtREAL;
consider s being object such that
A1: s in S by XBOOLE_0:def 1;
reconsider s as R_eal by A1;
assume S = Rainbow(p,G);
then S c= DYADIC by Th13;
then
A2: S c= [.a,b.] by URYSOHN2:28;
let e1 be R_eal;
assume e1 = 1;
then for x being ExtReal holds x in S implies x <= e1 by A2,
XXREAL_1:1;
then
A3: e1 is UpperBound of S by XXREAL_2:def 1;
0. <= s by A2,A1,XXREAL_1:1;
hence thesis by A3,A1,XXREAL_2:4,def 3;
end;
theorem Th15:
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
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A1: A <> {} & A misses B;
let G be Rain of A,B;
let r be Element of DOM;
let p be Point of T;
assume
A2: (Thunder G).p < r;
now
per cases;
suppose
A3: Rainbow(p,G) = {};
assume
A4: not p in (Tempest G).r;
r in halfline 0 \/ DYADIC or r in right_open_halfline 1 by URYSOHN1:def 3
,XBOOLE_0:def 3;
then
A5: r in halfline 0 or r in DYADIC or r in right_open_halfline 1 by
XBOOLE_0:def 3;
A6: 0 < r by A2,A3,Def6;
now
per cases by A6,A5,XXREAL_1:233;
suppose
A7: r in DYADIC;
reconsider r1 = r as R_eal by XXREAL_0:def 1;
A8: for s being Real st s = r1 holds not p in (Tempest G).s by A4;
then reconsider
S = Rainbow(p,G) as non empty Subset of ExtREAL by A7,Def5;
A9: (Thunder G).p = sup S by Def6;
r1 in Rainbow(p,G) by A7,A8,Def5;
hence thesis by A2,A9,XXREAL_2:4;
end;
suppose
r in right_open_halfline 1;
then (Tempest G).r = the carrier of T by A1,Def4;
hence thesis;
end;
end;
hence thesis;
end;
suppose
Rainbow(p,G) <> {};
then reconsider S = Rainbow(p,G) as non empty Subset of ExtREAL;
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
consider s being object such that
A10: s in S by XBOOLE_0:def 1;
reconsider s as R_eal by A10;
A11: s <= sup S by A10,XXREAL_2:4;
assume
A12: not p in (Tempest G).r;
r in halfline 0 \/ DYADIC or r in right_open_halfline 1 by URYSOHN1:def 3
,XBOOLE_0:def 3;
then
A13: r in halfline 0 or r in DYADIC or r in right_open_halfline 1 by
XBOOLE_0:def 3;
A14: (Thunder G).p = sup S by Def6;
for x being R_eal st x in S holds 0. <= x & x <= e1
proof
let x be R_eal;
assume x in S;
then
A15: x in DYADIC by Def5;
then reconsider x as Real;
ex n being Nat st x in dyadic(n) by A15,URYSOHN1:def 2;
hence thesis by URYSOHN1:1;
end;
then
A16: 0. <= s by A10;
now
per cases by A2,A14,A16,A11,A13,XXREAL_1:233;
suppose
A17: r in DYADIC;
reconsider r1 = r as R_eal by XXREAL_0:def 1;
for s being Real st s = r1 holds not p in (Tempest G).s by A12;
then r1 in Rainbow(p,G) by A17,Def5;
hence thesis by A2,A14,XXREAL_2:4;
end;
suppose
r in right_open_halfline 1;
then (Tempest G).r = the carrier of T by A1,Def4;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th16:
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
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A1: A <> {} & A misses B;
let G be Rain of A,B;
let r be Real;
assume that
A2: r in DYADIC \/ (right_open_halfline 1) and
A3: 0 < r;
let p be Point of T;
assume
A4: p in (Tempest G).r;
per cases by A2,XBOOLE_0:def 3;
suppose
A5: r in DYADIC;
then r in halfline 0 \/ DYADIC by XBOOLE_0:def 3;
then
A6: r in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
now
per cases;
case
Rainbow(p,G) = {};
hence thesis by A3,Def6;
end;
case
Rainbow(p,G) <> {};
then reconsider S = Rainbow(p,G) as non empty Subset of ExtREAL;
reconsider er = r as R_eal by XXREAL_0:def 1;
for r1 being ExtReal holds r1 in S implies r1 <= er
proof
let r1 be ExtReal;
assume
A7: r1 in S;
assume
A8: not r1 <= er;
A9: S c= DYADIC by Th13;
then r1 in DYADIC by A7;
then reconsider p1 = r1 as Real;
per cases;
suppose
A10: inf_number_dyadic(r) <= inf_number_dyadic(p1);
set n = inf_number_dyadic(p1);
r in dyadic(n) by A5,A10,Th6;
then
A11: (Tempest G).r = (G.n).r by A1,A5,A6,Def4;
reconsider D = G.n as Drizzle of A,B,n by A1,Def2;
p1 in halfline 0 \/ DYADIC by A7,A9,XBOOLE_0:def 3;
then
A12: p1 in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
p1 in dyadic(n) by A7,A9,Th5;
then
A13: (Tempest G).p1 = (G.n).p1 by A1,A7,A9,A12,Def4;
reconsider r,p1 as Element of dyadic(n) by A5,A7,A9,A10,Th6;
Cl(D.r) c= D.p1 & D.r c= Cl(D.r) by A1,A8,Def1,PRE_TOPC:18;
then D.r c= D.p1;
hence thesis by A4,A7,A11,A13,Def5;
end;
suppose
inf_number_dyadic(p1) <= inf_number_dyadic(r);
then
A14: dyadic(inf_number_dyadic(p1)) c= dyadic(inf_number_dyadic(r))
by URYSOHN2:29;
set n = inf_number_dyadic(r);
reconsider D = G.n as Drizzle of A,B,n by A1,Def2;
A15: p1 in dyadic(inf_number_dyadic(p1)) by A7,A9,Th5;
p1 in halfline 0 \/ DYADIC by A7,A9,XBOOLE_0:def 3;
then p1 in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
then
A16: (Tempest G).p1 = (G.n).p1 by A1,A7,A9,A15,A14,Def4;
r in dyadic(n) by A5,Th6;
then
A17: (Tempest G).r = (G.n).r by A1,A5,A6,Def4;
reconsider p1 as Element of dyadic(n) by A15,A14;
reconsider r as Element of dyadic(n) by A5,Th6;
Cl(D.r) c= D.p1 & D.r c= Cl(D.r) by A1,A8,Def1,PRE_TOPC:18;
then D.r c= D.p1;
hence thesis by A4,A7,A17,A16,Def5;
end;
end;
then r is UpperBound of S by XXREAL_2:def 1;
then sup S <= er by XXREAL_2:def 3;
hence thesis by Def6;
end;
end;
hence thesis;
end;
suppose
r in right_open_halfline 1;
then
A18: 1 < r by XXREAL_1:235;
now
per cases;
case
Rainbow(p,G) = {};
hence thesis by A18,Def6;
end;
case
A19: Rainbow(p,G) <> {};
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
consider S being non empty Subset of ExtREAL such that
A20: S = Rainbow(p,G) by A19;
sup S <= e1 & (Thunder G).p = sup S by A20,Def6,Th14;
hence thesis by A18,XXREAL_0:2;
end;
end;
hence thesis;
end;
end;
theorem Th17:
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
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A1: A <> {} & A misses B;
let G be Rain of A,B;
let r1 be Element of DOM;
assume
A2: 0 < r1;
let p be Point of T;
assume
A3: r1 < (Thunder G).p & p in (Tempest G).r1;
r1 in halfline 0 \/ DYADIC or r1 in right_open_halfline 1 by URYSOHN1:def 3
,XBOOLE_0:def 3;
then r1 in halfline 0 or r1 in DYADIC or r1 in right_open_halfline 1 by
XBOOLE_0:def 3;
then r1 in DYADIC \/ right_open_halfline 1 by A2,XBOOLE_0:def 3,XXREAL_1:233;
hence thesis by A1,A2,A3,Th16;
end;
theorem Th18:
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)
proof
A1: 1 in dyadic(0) by TARSKI:def 2,URYSOHN1:2;
then
A2: 1 in DYADIC by URYSOHN1:def 2;
then 1 in halfline 0 \/ DYADIC by XBOOLE_0:def 3;
then
A3: 1 in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A4: A <> {} & A misses B;
let G be Rain of A,B;
A5: 0 in dyadic(0) by TARSKI:def 2,URYSOHN1:2;
then
A6: 0 in DYADIC by URYSOHN1:def 2;
then 0 in halfline 0 \/ DYADIC by XBOOLE_0:def 3;
then
A7: 0 in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
A8: 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)
proof
let x be Point of T;
now
per cases;
case
A9: Rainbow(x,G) = {};
x in B implies (Thunder G).x = 1
proof
G.0 is Drizzle of A,B,0 by A4,Def2;
then
A10: B = [#]T \ (G.0).1 by A4,Def1;
assume
A11: x in B;
(Tempest G).1 = (G.0).1 by A4,A1,A2,A3,Def4;
then for s being Real st s = 1 holds not x in (Tempest G).s by A11
,A10,XBOOLE_0:def 5;
hence thesis by A9,Def5,URYSOHN2:27;
end;
hence thesis by A9,Def6;
end;
case
A12: Rainbow(x,G) <> {};
A13: x in A implies (Thunder G).x = 0
proof
assume
A14: x in A;
A15: for s being R_eal st 0. < s holds not s in Rainbow(x,G)
proof
let s be R_eal;
assume 0. < s;
assume
A16: s in Rainbow(x,G);
then
A17: s in DYADIC by Def5;
then reconsider s as Real;
consider n being Nat such that
A18: s in dyadic(n) by A17,URYSOHN1:def 2;
s in halfline 0 \/ DYADIC by A17,XBOOLE_0:def 3;
then s in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
then
A19: (Tempest G).s = (G.n).s by A4,A17,A18,Def4;
reconsider r1=0,r2=s as Element of dyadic(n) by A18,URYSOHN1:6;
reconsider D = G.n as Drizzle of A,B,n by A4,Def2;
per cases by A18,URYSOHN1:1;
suppose
A20: s = 0;
A c= D.0 by A4,Def1;
hence thesis by A14,A16,A19,A20,Def5;
end;
suppose
A21: 0 < s;
A22: D.r1 c= Cl(D.r1) by PRE_TOPC:18;
Cl(D.r1) c= D.r2 by A4,A21,Def1;
then
A23: D.r1 c= D.r2 by A22;
A c= D.0 by A4,Def1;
then A c= D.s by A23;
hence thesis by A14,A16,A19,Def5;
end;
end;
G.0 is Drizzle of A,B,0 by A4,Def2;
then
A24: A c= (G.0).0 by A4,Def1;
A25: (Tempest G).0 = (G.0).0 by A4,A5,A6,A7,Def4;
consider a being object such that
A26: a in Rainbow(x,G) by A12,XBOOLE_0:def 1;
A27: a in DYADIC by A26,Def5;
then reconsider a as Real;
A28: ex n being Nat st a in dyadic(n) by A27,URYSOHN1:def 2;
per cases by A28,URYSOHN1:1;
suppose
a = 0;
hence thesis by A14,A25,A24,A26,Def5;
end;
suppose
0 < a;
hence thesis by A15,A26;
end;
end;
reconsider S = Rainbow(x,G) as non empty Subset of ExtREAL by A12;
A29: sup S <= e1 by Th14;
A30: x in B implies (Thunder G).x = 1
proof
G.0 is Drizzle of A,B,0 by A4,Def2;
then
A31: B = [#]T \ (G.0).1 by A4,Def1;
assume
A32: x in B;
(Tempest G).1 = (G.0).1 by A4,A1,A2,A3,Def4;
then
A33: for s being Real st s = 1 holds not x in (Tempest G).s by A32,A31,
XBOOLE_0:def 5;
then reconsider S = Rainbow(x,G) as non empty Subset of ExtREAL by
Def5,URYSOHN2:27;
1 in Rainbow(x,G) by A33,Def5,URYSOHN2:27;
then
A34: e1 <= sup S by XXREAL_2:4;
(Thunder G).x = sup S by Def6;
hence thesis by A29,A34,XXREAL_0:1;
end;
e1 = 1 & (Thunder G).x = sup S by Def6;
hence thesis by A13,A30,Th14;
end;
end;
hence thesis;
end;
for p being Point of T holds Thunder(G) is_continuous_at p
proof
let p be Point of T;
for Q being Subset of R^1 st Q is open & (Thunder G).p in Q ex H
being Subset of T st H is open & p in H & (Thunder G).:H c= Q
proof
let Q be Subset of R^1;
assume that
A35: Q is open and
A36: (Thunder G).p in Q;
reconsider x = (Thunder G).p as Element of RealSpace by A36,TOPMETR:12
,def 6;
reconsider Q as Subset of REAL by TOPMETR:17;
the topology of R^1 = Family_open_set RealSpace & Q in the topology
of R^1 by A35,TOPMETR:12,def 6;
then consider r being Real such that
A37: r>0 and
A38: Ball(x,r) c= Q by A36,PCOMPS_1:def 4;
ex r0 being Real st r0 < r & 0 < r0 & r0 <= 1
proof
per cases;
suppose
A39: r <= 1;
consider r0 being Real such that
A40: 0 < r0 & r0 < r by A37,XREAL_1:5;
reconsider r0 as Real;
take r0;
thus thesis by A39,A40,XXREAL_0:2;
end;
suppose
1 < r;
hence thesis;
end;
end;
then consider r0 being Real such that
A41: r0 < r and
A42: 0 < r0 & r0 <= 1;
consider r1 being Real such that
A43: r1 in DYADIC and
A44: 0 < r1 and
A45: r1 < r0 by A42,URYSOHN2:24;
A46: r1 in DYADIC \/ right_open_halfline 1 by A43,XBOOLE_0:def 3;
consider n being Nat such that
A47: r1 in dyadic(n) by A43,URYSOHN1:def 2;
reconsider D = G.n as Drizzle of A,B,n by A4,Def2;
r1 in halfline 0 \/ DYADIC by A43,XBOOLE_0:def 3;
then
A48: r1 in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
then
A49: (Tempest G).r1 = (G.n).r1 by A4,A43,A47,Def4;
A50: r1 < r by A41,A45,XXREAL_0:2;
A51: for p being Point of T holds p in (Tempest G).r1 implies (Thunder G
).p < r
proof
let p be Point of T;
assume p in (Tempest G).r1;
then (Thunder G).p <= r1 by A4,A44,A46,Th16;
hence thesis by A50,XXREAL_0:2;
end;
A52: the carrier of R^1 = the carrier of RealSpace by TOPMETR:12,def 6;
reconsider r1 as Element of dyadic(n) by A47;
reconsider H = D.r1 as Subset of T;
A53: 0 in dyadic(n) by URYSOHN1:6;
ex H being Subset of T st H is open & p in H & (Thunder G).:H c= Q
proof
per cases;
suppose
A54: x = 0;
take H;
(Thunder G).:H c= Q
proof
reconsider p = x as Real;
let y be object;
assume y in (Thunder G).:H;
then consider x1 being object such that
x1 in dom (Thunder G) and
A55: x1 in H and
A56: y = (Thunder G).x1 by FUNCT_1:def 6;
reconsider y as Point of RealSpace by A52,A55,A56,FUNCT_2:5;
reconsider q = y as Real;
A57: -(p - q) < r by A51,A49,A54,A55,A56;
reconsider x1 as Point of T by A55;
A58: 0 <= (Thunder G).x1 by A8;
A59: q - p < r - 0 by A51,A49,A54,A55,A56;
then
p - q < r by A54,A56,A58,XREAL_1:14;
then A60: |.p-q.| <> r by A57,ABSVALUE:def 1;
A61: dist(x,y) < r implies y in Ball(x,r) by METRIC_1:11;
--(p - q) = p - q;
then -r < p - q by A57,XREAL_1:24;
then dist(x,y) = |.p-q.| & |.p-q.| <= r by A54,A56,A58,A59,
ABSVALUE:5,TOPMETR:11;
hence thesis by A38,A61,A60,XXREAL_0:1;
end;
hence thesis by A4,A44,A48,A49,A53,A54,Def1,Th15;
end;
suppose
A62: x <> 0;
reconsider x as Real;
0 <= (Thunder G).p by A8;
then consider r1,r2 being Real such that
A63: r1 in DYADIC \/ right_open_halfline 1 and
r2 in DYADIC \/ right_open_halfline 1 and
A64: 0 < r1 and
A65: r1 < x and
A66: x < r2 and
A67: r2 - r1 < r by A37,A62,URYSOHN2:31;
r1 in DYADIC or r1 in right_open_halfline 1 by A63,XBOOLE_0:def 3;
then r1 in halfline 0 \/ DYADIC or r1 in right_open_halfline 1 by
XBOOLE_0:def 3;
then
A68: r1 in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
then reconsider B = (Tempest G).r1 as Subset of T by FUNCT_2:5;
reconsider C = [#]T \ Cl B as Subset of T;
consider r3 being Real such that
A69: r3 in DOM and
A70: x < r3 and
A71: r3 < r2 by A66,URYSOHN2:25;
Cl(Cl B) = Cl B;
then Cl B is closed by PRE_TOPC:22;
then
A72: C is open;
reconsider A = (Tempest G).r3 as Subset of T by A69,FUNCT_2:5;
take H = A /\ C;
A73: (Thunder G).:H c= Q
proof
reconsider x as Element of RealSpace;
let y be object;
reconsider p = x as Real;
assume y in (Thunder G).:H;
then consider x1 being object such that
x1 in dom (Thunder G) and
A74: x1 in H and
A75: y = (Thunder G).x1 by FUNCT_1:def 6;
reconsider x1 as Point of T by A74;
A76: x1 in (Tempest G).r3 by A74,XBOOLE_0:def 4;
reconsider y as Real by A75;
reconsider y as Point of RealSpace by A52,A74,A75,FUNCT_2:5;
reconsider q = y as Real;
A77: -(-(p - q)) = p - q;
A78: not r3 <= 0 by A8,A70;
r3 in halfline 0 \/ DYADIC or r3 in right_open_halfline 1 by A69,
URYSOHN1:def 3,XBOOLE_0:def 3;
then r3 in halfline 0 or r3 in DYADIC or r3 in
right_open_halfline 1 by XBOOLE_0:def 3;
then r3 in DYADIC \/ right_open_halfline 1 by A78,XBOOLE_0:def 3
,XXREAL_1:233;
then (Thunder G).x1 <= r3 by A4,A76,A78,Th16;
then (Thunder G).x1 < r2 by A71,XXREAL_0:2;
then
A79: q - p < r2 - r1 by A65,A75,XREAL_1:14;
then -(p - q) < r by A67,XXREAL_0:2;
then
A80: -r < p - q by A77,XREAL_1:24;
A81: x1 in [#]T \ Cl B by A74,XBOOLE_0:def 4;
not x1 in B
proof
A82: B c= Cl B by PRE_TOPC:18;
assume x1 in B;
hence thesis by A81,A82,XBOOLE_0:def 5;
end;
then
A83: p - q < r2 - r1 by A4,A66,A68,A75,Th15,XREAL_1:14;
then p - q < r by A67,XXREAL_0:2;
then
A84: dist(x,y) = |.p-q.| & |.p-q.| <= r by A80,ABSVALUE:5,TOPMETR:11;
A85: |.p-q.| <> r
proof
assume
A86: |.p-q.| = r;
per cases;
suppose
0 <= p - q;
hence thesis by A67,A83,A86,ABSVALUE:def 1;
end;
suppose
p - q < 0;
then |.p-q.| = -(p - q) by ABSVALUE:def 1;
hence thesis by A67,A79,A86;
end;
end;
dist(x,y) < r implies y in Ball(x,r) by METRIC_1:11;
hence thesis by A38,A84,A85,XXREAL_0:1;
end;
(Thunder G).p <= 1 by A8;
then consider r4 being Real such that
A87: r4 in DYADIC and
A88: r1 < r4 and
A89: r4 < x by A64,A65,URYSOHN2:24;
A90: r4 in halfline 0 \/ DYADIC by A87,XBOOLE_0:def 3;
then r4 in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
then
A91: Cl B c= (Tempest G).r4 by A4,A88,A68,Th12;
reconsider r4 as Element of DOM by A90,URYSOHN1:def 3,XBOOLE_0:def 3;
not p in (Tempest G).r4 by A4,A64,A88,A89,Th17;
then not p in Cl B by A91;
then
A92: p in C by XBOOLE_0:def 5;
A is open & p in (Tempest G).r3 by A4,A69,A70,Th11,Th15;
hence thesis by A72,A92,A73,TOPS_1:11,XBOOLE_0:def 4;
end;
end;
hence thesis;
end;
hence thesis by TMAP_1:43;
end;
hence thesis by A8,TMAP_1:44;
end;
theorem Th19:
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)
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A1: A <> {} & A misses B;
set R = the Rain of A,B;
take Thunder(R);
thus thesis by A1,Th18;
end;
::$N Urysohn's lemma
::$L https://en.wikipedia.org/wiki/Urysohn's_lemma Urysohn's lemma
theorem Th20:
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)
proof
let T be non empty normal TopSpace;
let A,B be closed Subset of T;
assume
A1: A misses B;
per cases;
suppose
A <> {};
hence thesis by A1,Th19;
end;
suppose
A2: A = {};
set S = the carrier of T, L = the carrier of R^1;
1 in REAL by XREAL_0:def 1;
then reconsider r = 1 as Element of L by TOPMETR:17;
defpred P[set,set] means $2 = r;
A3: for x being Element of S ex y being Element of L st P[x,y];
ex F being Function of S,L st for x being Element of S holds P[x,F.x]
from FUNCT_2:sch 3(A3);
then consider F being Function of S,L such that
A4: for x being Element of S holds F.x = r;
take F;
A5: dom F = the carrier of T by FUNCT_2:def 1;
thus F is continuous
proof
the carrier of T c= the carrier of T;
then reconsider O1 = the carrier of T as Subset of T;
reconsider O2 = {} as Subset of T by XBOOLE_1:2;
let P be Subset of R^1;
assume P is closed;
A6: O2 is closed;
per cases;
suppose
1 in P;
then for x being object
holds x in the carrier of T iff x in dom F & F.x
in P by A4,FUNCT_2:def 1;
hence thesis by FUNCT_1:def 7;
end;
suppose
not 1 in P;
then for x being object
holds x in {} iff x in dom F & F.x in P by A4,A5;
hence thesis by A6,FUNCT_1:def 7;
end;
end;
let x be Point of T;
thus thesis by A2,A4;
end;
end;
theorem
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) by Th20;
:: 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.