:: The Theorem of Weierstrass
:: by J\'ozef Bia\las and Yatsuka Nakamura
::
:: Received July 10, 1995
:: Copyright (c) 1995-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, METRIC_1, PRE_TOPC, REAL_1, XBOOLE_0, TARSKI, COMPLEX1,
ARYTM_3, XXREAL_0, CARD_1, ARYTM_1, NAT_1, SETFAM_1, FINSEQ_1, TOPMETR,
RELAT_1, FINSET_1, FUNCT_1, ORDINAL2, RCOMP_1, SUBSET_1, ZFMISC_1,
EUCLID, XXREAL_2, STRUCT_0, PCOMPS_1, SEQ_1, SEQ_2, VALUED_0, SEQ_4,
WEIERSTR;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2,
BINOP_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1,
REAL_1, NAT_1, TOPMETR, METRIC_1, COMPTS_1, SEQ_1, SEQ_2, VALUED_0,
SEQ_4, FINSEQ_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_2, RCOMP_1, EUCLID,
PCOMPS_1, XXREAL_0, XXREAL_2;
constructors REAL_1, COMPLEX1, SEQ_2, SEQ_4, RCOMP_1, TOPS_2, COMPTS_1,
EUCLID, TOPMETR, BINOP_2, PCOMPS_1, COMSEQ_2, BINOP_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS,
XREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, TOPMETR,
FINSEQ_1;
requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XXREAL_2;
equalities STRUCT_0;
expansions TARSKI, XXREAL_2;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, FINSEQ_1, ZFMISC_1, SEQ_2, SEQ_4,
ABSVALUE, COMPTS_1, RELAT_1, TOPS_2, RCOMP_1, TOPMETR, PCOMPS_1,
METRIC_1, METRIC_6, XBOOLE_0, XBOOLE_1, XREAL_0, SUBSET_1, XREAL_1,
COMPLEX1, XXREAL_0, SETFAM_1;
schemes NAT_1, SUBSET_1, FUNCT_2;
begin
theorem Th1:
for M being MetrSpace, x1,x2 being Point of M, r1,r2 being Real
ex x being Point of M, r being Real
st Ball(x1,r1) \/ Ball(x2,r2) c= Ball(x,r)
proof
let M be MetrSpace;
let x1,x2 be Point of M;
let r1,r2 be Real;
reconsider x = x1 as Point of M;
reconsider r = |.r1.| + |.r2.| + dist(x1,x2) as Real;
take x;
take r;
for a being object
holds a in Ball(x1,r1) \/ Ball(x2,r2) implies a in Ball( x,r)
proof
let a be object;
assume
A1: a in (Ball(x1,r1) \/ Ball(x2,r2));
then reconsider a as Point of M;
now
per cases by A1,XBOOLE_0:def 3;
case
A2: a in Ball(x1,r1);
r1 <= |.r1.| & 0 <= |.r2.| by ABSVALUE:4,COMPLEX1:46;
then
A3: r1 + 0 <= |.r1.| + |.r2.| by XREAL_1:7;
A4: dist(x,a) < r1 by A2,METRIC_1:11;
0 <= dist(x1,x2) by METRIC_1:5;
then r1 + 0 <= |.r1.| + |.r2.| + dist(x1,x2) by A3,XREAL_1:7;
then dist(x,a) - r < r1 - r1 by A4,XREAL_1:14;
then
A5: dist(x,a) - r + r < 0 + r by XREAL_1:8;
M is non empty by A2;
hence thesis by A5,METRIC_1:11;
end;
case
A6: a in Ball(x2,r2);
then dist(x2,a) < r2 by METRIC_1:11;
then dist(x2,a) - |.r2.| < r2 - r2 by ABSVALUE:4,XREAL_1:14;
then dist(x,a) <= dist(x1,x2) + dist(x2,a) & dist(x2,a) - |.r2.| +
|.r2.| < 0 + |.r2.| by METRIC_1:4,XREAL_1:8;
then dist(x,a) - |.r2.| < dist(x1,x2) + dist(x2,a) - dist(x2,a ) by
XREAL_1:15;
then dist(x,a) - |.r2.| - |.r1.| < dist(x1,x2) - 0 by COMPLEX1:46
,XREAL_1:14;
then
A7: dist(x,a) - (|.r1.| + |.r2.|) + (|.r1.| + |.r2.|) < |.r1.| +
|.r2.| + dist(x1,x2) by XREAL_1:8;
M is non empty by A6;
hence thesis by A7,METRIC_1:11;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th2:
for M being MetrSpace, n being Nat, F being Subset-Family of M, p
being FinSequence st F is being_ball-family & rng p = F & dom p = Seg(n+1)
holds ex G being Subset-Family of M st (G is finite & G is being_ball-family &
ex q being FinSequence st rng q = G & dom q = Seg(n) & ex x being Point of M st
ex r being Real st union F c= union G \/ Ball(x,r) )
proof
let M be MetrSpace;
let n be Nat;
let F be Subset-Family of M;
let p be FinSequence;
assume that
A1: F is being_ball-family and
A2: rng p = F and
A3: dom p = Seg(n+1);
n+1 in dom p by A3,FINSEQ_1:4;
then p.(n+1) in F by A2,FUNCT_1:def 3;
then consider x being Point of M such that
A4: ex r being Real st p.(n+1) = Ball(x,r) by A1,TOPMETR:def 4;
consider r being Real such that
A5: p.(n+1) = Ball(x,r) by A4;
reconsider q = p|(Seg(n)) as FinSequence by FINSEQ_1:15;
A6: rng q c= rng p by RELAT_1:70;
then reconsider G=rng q as Subset-Family of M by A2,XBOOLE_1:1;
reconsider G as Subset-Family of M;
len p = n+1 by A3,FINSEQ_1:def 3;
then n <= len p by NAT_1:11;
then
A7: dom q = Seg(n) by FINSEQ_1:17;
then
A8: dom q \/ {n+1} = dom p by A3,FINSEQ_1:9;
A9: ex x being Point of M st
ex r being Real st union F c= union G \/ Ball(x,r)
proof
take x;
reconsider r as Real;
take r;
union F c= union G \/ Ball(x,r)
proof
let t be object;
assume t in union F;
then consider A being set such that
A10: t in A and
A11: A in F by TARSKI:def 4;
consider s being object such that
A12: s in dom p and
A13: A = p.s by A2,A11,FUNCT_1:def 3;
now
per cases by A8,A12,XBOOLE_0:def 3;
case
s in dom q;
then q.s in G & q.s = A by A13,FUNCT_1:47,def 3;
then
A14: t in union G by A10,TARSKI:def 4;
union G c= union G \/ Ball(x,r) by XBOOLE_1:7;
hence thesis by A14;
end;
case
s in {n+1};
then p.s = Ball(x,r) by A5,TARSKI:def 1;
hence thesis by A10,A13,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
hence thesis;
end;
take G;
for x being set holds x in G implies ex y being Point of M st
ex r being Real st x = Ball(y,r) by A1,A2,A6,TOPMETR:def 4;
hence thesis by A7,A9,TOPMETR:def 4;
end;
theorem Th3:
for M being MetrSpace, F being Subset-Family of M st F is finite
& F is being_ball-family holds ex x being Point of M, r being Real st union F
c= Ball(x,r)
proof
let M be MetrSpace;
let F be Subset-Family of M;
assume that
A1: F is finite and
A2: F is being_ball-family;
consider p being FinSequence such that
A3: rng p = F by A1,FINSEQ_1:52;
A4: for F being Subset-Family of M st F is finite & F is being_ball-family
holds for n being Nat holds for p being FinSequence st rng p = F & dom p = Seg
n holds ex x being Point of M, r being Real st union F c= Ball(x,r)
proof
defpred P[Nat] means for F being Subset-Family of M st (F is finite & F is
being_ball-family) holds for n being Nat st n = $1 holds for p being
FinSequence st (rng p = F & dom p = Seg(n)) holds (ex x being Point of M st ex
r being Real st union F c= Ball(x,r));
A5: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A6: P[k];
let F be Subset-Family of M;
assume that
F is finite and
A7: F is being_ball-family;
let n be Nat;
assume
A8: n = k+1;
let p be FinSequence;
assume rng p = F & dom p = Seg(n);
then consider F1 being Subset-Family of M such that
A9: F1 is finite & F1 is being_ball-family and
A10: ex p1 being FinSequence st rng p1 = F1 & dom p1 = Seg(k) & ex
x2 being Point of M st ex r2 being Real st union F c= union F1 \/ Ball(x2,r2)
by A7,A8,Th2;
consider x1 being Point of M such that
A11: ex r being Real st union F1 c= Ball(x1,r) by A6,A9,A10;
consider x2 being Point of M such that
A12: ex r2 being Real st union F c= union F1 \/ Ball(x2,r2) by A10;
consider r2 being Real such that
A13: union F c= union F1 \/ Ball(x2,r2) by A12;
consider r1 being Real such that
A14: union F1 c= Ball(x1,r1) by A11;
consider x being Point of M such that
A15: ex r being Real st Ball(x1,r1) \/ Ball(x2,r2) c= Ball(x,r) by Th1;
take x;
consider r being Real such that
A16: Ball(x1,r1) \/ Ball(x2,r2) c= Ball(x,r) by A15;
reconsider r as Real;
take r;
union F1 \/ Ball(x2,r2) c= Ball(x1,r1) \/ Ball(x2,r2) by A14,XBOOLE_1:9;
then union F c= Ball(x1,r1) \/ Ball(x2,r2) by A13;
hence thesis by A16;
end;
A17: P[0]
proof
let F be Subset-Family of M;
assume that
F is finite and
F is being_ball-family;
let n be Nat;
assume n = 0;
then
A18: Seg n = {};
for p being FinSequence st rng p = F & dom p = Seg(n) holds ex x
being Point of M st ex r being Real st union F c= Ball(x,r)
proof
set x = the Point of M;
let p be FinSequence;
assume
A19: rng p = F & dom p = Seg(n);
take x, 0;
union F = {} by A19,A18,RELAT_1:42,ZFMISC_1:2;
hence thesis;
end;
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A17,A5);
hence thesis;
end;
ex n being Nat st dom p = Seg n by FINSEQ_1:def 2;
hence thesis by A2,A4,A3;
end;
theorem Th4:
for T,S being non empty TopSpace, f being Function of T,S, B
being Subset-Family of S st f is continuous & B is open holds f"B is open
proof
let T,S be non empty TopSpace;
let f be Function of T,S;
let B be Subset-Family of S;
assume that
A1: f is continuous and
A2: B is open;
for P being Subset of T holds P in f"B implies P is open
proof
let P be Subset of T;
assume
A3: P in f"(B);
thus P is open
proof
consider C being Subset of S such that
A4: C in B and
A5: P = f"C by A3,FUNCT_2:def 9;
reconsider C as Subset of S;
[#]S <> {} & C is open by A2,A4,TOPS_2:def 1;
hence thesis by A1,A5,TOPS_2:43;
end;
end;
hence thesis by TOPS_2:def 1;
end;
theorem
for T,S being non empty TopSpace holds for f being Function of T,S
holds for Q being Subset-Family of S holds Q is finite implies f"Q is finite
proof
let T,S be non empty TopSpace;
let f be Function of T,S;
let Q be Subset-Family of S;
defpred EF[Subset of [#](S),Subset of [#](T)] means for s,t being set holds
($1 = s & $2 = t implies t = f"s);
assume Q is finite;
then consider s being FinSequence such that
A1: rng s = Q by FINSEQ_1:52;
A2: for x being Subset of [#](S) ex y being Subset of [#](T) st EF[x,y]
proof
let x be Subset of [#](S);
reconsider x as set;
set y = f"x;
reconsider y as Subset of [#](T);
take y;
thus thesis;
end;
consider F being Function of bool [#](S),bool [#](T) such that
A3: for x being Subset of [#](S) holds EF[x,F.x qua Subset of [#](T)]
from FUNCT_2:sch 3 (A2);
dom F = bool [#](S) by FUNCT_2:def 1;
then reconsider q = F*s as FinSequence by A1,FINSEQ_1:16;
for x being object holds x in F.:Q iff x in f"Q
proof
let x be object;
A4: dom F = bool [#](S) by FUNCT_2:def 1;
thus x in F.:Q implies x in f"Q
proof
assume x in F.:Q;
then consider y being object such that
A5: y in dom F and
A6: y in Q & x = F.y by FUNCT_1:def 6;
reconsider y as Subset of S by A5;
F.y = f"y by A3;
hence thesis by A6,FUNCT_2:def 9;
end;
assume
A7: x in f"Q;
then reconsider x as Subset of T;
consider y being Subset of S such that
A8: y in Q and
A9: x = f"y by A7,FUNCT_2:def 9;
x = F.y by A3,A9;
hence thesis by A8,A4,FUNCT_1:def 6;
end;
then
A10: F.:Q = f"Q by TARSKI:2;
ex q being FinSequence st rng q = f"Q
proof
take q;
thus thesis by A1,A10,RELAT_1:127;
end;
hence thesis;
end;
theorem
for T,S being non empty TopSpace holds for f being Function of T,S
holds for P being Subset-Family of T holds P is finite implies f.:P is finite
proof
let T,S be non empty TopSpace;
let f be Function of T,S;
let P be Subset-Family of T;
defpred EF[Subset of [#](T),Subset of [#](S)] means for s,t being set holds
($1 = s & $2 = t implies t = f.:s);
assume P is finite;
then consider s being FinSequence such that
A1: rng s = P by FINSEQ_1:52;
A2: for x being Subset of [#](T) ex y being Subset of [#](S) st EF[x,y]
proof
let x be Subset of [#](T);
reconsider x as set;
set y = f.:x;
reconsider y as Subset of [#](S);
take y;
thus thesis;
end;
consider F being Function of bool [#](T),bool [#](S) such that
A3: for x being Subset of [#](T) holds EF[x,F.x qua Subset of [#](S)]
from FUNCT_2:sch 3 (A2);
dom F = bool [#](T) by FUNCT_2:def 1;
then reconsider q = F*s as FinSequence by A1,FINSEQ_1:16;
for x being object holds x in F.:P iff x in f.:P
proof
let x be object;
thus x in F.:P implies x in f.:P
proof
assume x in F.:P;
then consider y being object such that
A4: y in dom F and
A5: y in P & x = F.y by FUNCT_1:def 6;
reconsider y as Subset of T by A4;
F.y = f.:y by A3;
hence thesis by A5,FUNCT_2:def 10;
end;
thus x in f.:P implies x in F.:P
proof
assume
A6: x in f.:P;
then reconsider x as Subset of S;
consider y being Subset of T such that
A7: y in P and
A8: x = f.:y by A6,FUNCT_2:def 10;
A9: dom F = bool [#](T) by FUNCT_2:def 1;
x = F.y by A3,A8;
hence thesis by A7,A9,FUNCT_1:def 6;
end;
end;
then
A10: F.:P = f.:P by TARSKI:2;
ex q being FinSequence st rng q = f.:P
proof
take q;
thus thesis by A1,A10,RELAT_1:127;
end;
hence thesis;
end;
theorem Th7:
for T,S being non empty TopSpace holds for f being Function of T
,S holds for P being Subset of T holds for F being Subset-Family of S holds (ex
B being Subset-Family of T st (B c= f"F & B is Cover of P & B is finite))
implies ex G being Subset-Family of S st G c= F & G is Cover of f.:P & G is
finite
proof
let T,S be non empty TopSpace;
let f be Function of T,S;
let P be Subset of T;
let F be Subset-Family of S;
given B being Subset-Family of T such that
A1: B c= f"F and
A2: B is Cover of P and
A3: B is finite;
A4: P c= union B by A2,SETFAM_1:def 11;
now
per cases;
case
A5: P <> {};
thus ex G being Subset-Family of S st G c= F & G is Cover of f.:P &
G is finite
proof
consider s being FinSequence such that
A6: rng s = B by A3,FINSEQ_1:52;
B <> {} by A4,A5,ZFMISC_1:2;
then consider D being non empty set such that
A7: D = B;
defpred P0[Element of D,Subset of [#](S)] means for x being Element of
D st $1 = x holds for y being Subset of [#](S) st $2 = y holds (y in F & x = f"
y);
A8: for x being Element of D ex y being Subset of [#](S) st P0[x,y]
proof
let x be Element of D;
A9: x in B by A7;
then reconsider x as Subset of T;
consider y being Subset of S such that
A10: y in F & x = f"y by A1,A9,FUNCT_2:def 9;
reconsider y as Subset of [#](S);
take y;
thus thesis by A10;
end;
consider F0 being Function of D,bool [#](S) such that
A11: for x being Element of D holds P0[x,F0.x qua Subset of [#](S)
] from FUNCT_2:sch 3(A8);
A12: for x being Element of D holds F0.x in F & x = f"(F0.x) by A11;
reconsider F0 as Function of B,bool [#](S) by A7;
A13: dom F0 = B by FUNCT_2:def 1;
then reconsider q = F0*s as FinSequence by A6,FINSEQ_1:16;
set G = rng q;
A14: G c= F
proof
let x be object;
assume x in G;
then consider y being object such that
A15: y in dom q & x = q.y by FUNCT_1:def 3;
s.y in B & x = F0.(s.y) by A13,A15,FUNCT_1:11,12;
hence thesis by A7,A12;
end;
then reconsider G as Subset-Family of S by XBOOLE_1:1;
reconsider G as Subset-Family of S;
take G;
for x being object holds x in f.:P implies x in union G
proof
let x be object;
assume
A16: x in f.:P;
ex A being set st x in A & A in G
proof
consider y being object such that
A17: y in dom f and
A18: y in P and
A19: x = f.y by A16,FUNCT_1:def 6;
consider C being set such that
A20: y in C and
A21: C in B by A4,A18,TARSKI:def 4;
C = f"(F0.C) by A7,A12,A21;
then
A22: x in f.:(f"(F0.C)) by A17,A19,A20,FUNCT_1:def 6;
set A = F0.C;
take A;
f.:(f"(F0.C)) c= F0.C & G = rng F0 by A6,A13,FUNCT_1:75,RELAT_1:28;
hence thesis by A21,A22,FUNCT_2:4;
end;
hence thesis by TARSKI:def 4;
end;
then f.:P c= union G;
hence thesis by A14,SETFAM_1:def 11;
end;
hence thesis;
end;
case
A23: P = {};
ex G being Subset-Family of S st G c= F & G is Cover of f.:P & G is
finite
proof
set G = {};
reconsider G as Subset-Family of S by XBOOLE_1:2;
reconsider G as Subset-Family of S;
take G;
f.:P = {}
proof
assume f.:P <> {};
then consider x being object such that
A24: x in f.:P by XBOOLE_0:def 1;
ex z being object st z in dom f & z in P & x = f.z
by A24,FUNCT_1:def 6;
hence contradiction by A23;
end;
hence thesis by SETFAM_1:def 11,ZFMISC_1:2;
end;
hence thesis;
end;
end;
hence thesis;
end;
begin
::
:: The Weierstrass` theorem
::
theorem Th8:
for T,S being non empty TopSpace holds for f being Function of T
,S holds for P being Subset of T holds P is compact & f is continuous implies f
.:P is compact
proof
let T,S be non empty TopSpace;
let f be Function of T,S;
let P be Subset of T;
assume that
A1: P is compact and
A2: f is continuous;
P c= [#]T;
then
A3: P c= dom f by FUNCT_2:def 1;
for F0 being Subset-Family of S st F0 is Cover of f.:P & F0 is open ex G
being Subset-Family of S st G c= F0 & G is Cover of f.:P & G is finite
proof
let F0 be Subset-Family of S;
assume that
A4: F0 is Cover of f.:P and
A5: F0 is open;
set B0 = f"F0;
A6: f.:P c= union F0 by A4,SETFAM_1:def 11;
P c= union B0
proof
let x be object;
thus x in P implies x in union B0
proof
A7: f"(union F0) c= union(f"F0)
proof
let y be object;
assume
A8: y in f"(union F0);
thus y in union(f"F0)
proof
f.y in union F0 by A8,FUNCT_1:def 7;
then consider Q being set such that
A9: f.y in Q & Q in F0 by TARSKI:def 4;
A10: y in dom f by A8,FUNCT_1:def 7;
ex Z being set st y in Z & Z in f"F0
proof
set Z = f"Q;
take Z;
thus thesis by A10,A9,FUNCT_1:def 7,FUNCT_2:def 9;
end;
hence thesis by TARSKI:def 4;
end;
end;
assume
A11: x in P;
then
A12: f.x in f.:P by A3,FUNCT_1:def 6;
reconsider x as Point of T by A11;
A13: f.x in union F0 by A6,A12;
A14: f"{f.x} c= f"(union F0)
proof
let y be object;
assume
A15: y in f"{f.x};
then f.y in {f.x} by FUNCT_1:def 7;
then
A16: f.y in union F0 by A13,TARSKI:def 1;
y in dom f by A15,FUNCT_1:def 7;
hence thesis by A16,FUNCT_1:def 7;
end;
f.x in {f.x} by TARSKI:def 1;
then x in f"{f.x} by A3,A11,FUNCT_1:def 7;
then x in f"(union F0) by A14;
hence thesis by A7;
end;
end;
then
A17: B0 is Cover of P by SETFAM_1:def 11;
B0 is open by A2,A5,Th4;
then ex B being Subset-Family of T st B c= B0 & B is Cover of P & B is
finite by A1,A17,COMPTS_1:def 4;
then consider G being Subset-Family of S such that
A18: G c= F0 & G is Cover of f.:P & G is finite by Th7;
take G;
thus thesis by A18;
end;
hence thesis by COMPTS_1:def 4;
end;
theorem
for T being non empty TopSpace holds for f being Function of T,R^1
holds for P being Subset of T holds P is compact & f is continuous implies f.:P
is compact by Th8;
theorem
for f being Function of TOP-REAL 2,R^1 holds for P being Subset of
TOP-REAL 2 holds P is compact & f is continuous implies f.:P is compact by Th8;
definition
let P be Subset of R^1;
func [#](P) -> Subset of REAL equals
P;
correctness by TOPMETR:17;
end;
theorem Th11:
for P being Subset of R^1 holds P is compact implies [#](P) is real-bounded
proof
let P be Subset of R^1;
assume
A1: P is compact;
thus [#](P) is real-bounded
proof
now
per cases;
case
[#](P) <> {};
set r0 = 1;
defpred P[Subset of R^1] means ex x being Point of RealSpace st x in
[#](P) & $1 = Ball(x,r0);
consider R being Subset-Family of R^1 such that
A2: for A being Subset of R^1 holds A in R iff P[A] from SUBSET_1:
sch 3;
for x being object holds x in [#](P) implies x in union R
proof
let x be object;
assume
A3: x in [#](P);
then reconsider x as Point of RealSpace by METRIC_1:def 13;
consider A being Subset of RealSpace such that
A4: A = Ball(x,r0);
R^1 = TopStruct (#the carrier of RealSpace, Family_open_set(
RealSpace)#) by PCOMPS_1:def 5,TOPMETR:def 6;
then reconsider A as Subset of R^1;
ex A being set st x in A & A in R
proof
take A;
dist(x,x) = 0 by METRIC_1:1;
hence thesis by A2,A3,A4,METRIC_1:11;
end;
hence thesis by TARSKI:def 4;
end;
then [#](P) c= union R;
then
A5: R is Cover of P by SETFAM_1:def 11;
for A being Subset of R^1 holds A in R implies A is open
proof
let A be Subset of R^1;
assume A in R;
then
ex x being Point of RealSpace st x in [#](P) & A = Ball(x,r0) by A2;
hence thesis by TOPMETR:14,def 6;
end;
then R is open by TOPS_2:def 1;
then consider R0 being Subset-Family of R^1 such that
A6: R0 c= R and
A7: R0 is Cover of P and
A8: R0 is finite by A1,A5,COMPTS_1:def 4;
A9: P c= union R0 by A7,SETFAM_1:def 11;
A10: for A being set holds A in R0 implies ex x being Point of
RealSpace,r being Real st A = Ball(x,r)
proof
let A be set;
assume
A11: A in R0;
then reconsider A as Subset of R^1;
consider x being Point of RealSpace such that
x in [#](P) and
A12: A = Ball(x,r0) by A2,A6,A11;
take x;
take r0;
thus thesis by A12;
end;
R^1 = TopStruct (#the carrier of RealSpace, Family_open_set(
RealSpace)#) by PCOMPS_1:def 5,TOPMETR:def 6;
then reconsider R0 as Subset-Family of RealSpace;
R0 is being_ball-family by A10,TOPMETR:def 4;
then consider x1 being Point of RealSpace such that
A13: ex r1 being Real st union R0 c= Ball(x1,r1) by A8,Th3;
consider r1 being Real such that
A14: union R0 c= Ball(x1,r1) by A13;
A15: [#](P) c= Ball(x1,r1) by A9,A14;
reconsider x1 as Element of REAL by METRIC_1:def 13;
A16: for p being Element of REAL
holds p in [#](P) implies x1 - r1 <= p & p <= x1 + r1
proof
let p be Element of REAL;
reconsider a=x1,b=p as Element of RealSpace by METRIC_1:def 13;
assume p in [#](P);
then dist(a,b) < r1 by A15,METRIC_1:11;
then
A17: |.x1-p.| < r1 by TOPMETR:11;
then -r1 <= x1 - p by ABSVALUE:5;
then -r1 + p <= x1 by XREAL_1:19;
then
A18: p <= x1 -(-r1) by XREAL_1:19;
x1 - p <= r1 by A17,ABSVALUE:5;
then x1 <= p + r1 by XREAL_1:20;
hence thesis by A18,XREAL_1:20;
end;
x1 - r1 is LowerBound of [#]P
proof
let r be ExtReal;
thus thesis by A16;
end;
then
A19: [#](P) is bounded_below;
x1 + r1 is UpperBound of [#]P
proof
let r be ExtReal;
thus thesis by A16;
end;
then [#](P) is bounded_above;
hence thesis by A19;
end;
case
A20: [#](P) = {};
0 is LowerBound of [#]P
proof
let r be ExtReal;
thus thesis by A20;
end;
then
A21: [#](P) is bounded_below;
0 is UpperBound of [#]P
proof
let r be ExtReal;
thus thesis by A20;
end;
then [#](P) is bounded_above;
hence thesis by A21;
end;
end;
hence thesis;
end;
end;
theorem Th12:
for P being Subset of R^1 holds P is compact implies [#](P) is closed
proof
let P be Subset of R^1;
assume
A1: P is compact;
now
per cases;
case
A2: [#](P) <> {};
A3: R^1 is T_2 by PCOMPS_1:34,TOPMETR:def 6;
for s1 being Real_Sequence st (rng s1) c= [#](P) & s1 is convergent
holds lim s1 in [#](P)
proof
let s1 be Real_Sequence;
assume that
A4: (rng s1) c= [#](P) and
A5: s1 is convergent;
set x = lim s1;
x in REAL by XREAL_0:def 1;
then reconsider x as Point of R^1 by TOPMETR:17;
thus lim s1 in [#](P)
proof
assume not lim s1 in [#](P);
then x in P` by SUBSET_1:29;
then consider Otx,OtP being Subset of R^1 such that
A6: Otx is open and
OtP is open and
A7: x in Otx and
A8: P c= OtP & Otx misses OtP by A1,A2,A3,COMPTS_1:6;
A9: R^1 = TopStruct (#the carrier of RealSpace, Family_open_set(
RealSpace)#) by PCOMPS_1:def 5,TOPMETR:def 6;
then reconsider x as Point of RealSpace;
consider r being Real such that
A10: r>0 and
A11: Ball(x,r) c= Otx by A6,A7,TOPMETR:15,def 6;
reconsider r as Real;
A12: Ball(x,r) = {q where q is Element of RealSpace :dist(x,q)<r} by
METRIC_1:17;
(rng s1) misses Otx by A4,A8,XBOOLE_1:1,63;
then
A13: Ball(x,r) misses (rng s1) by A11,XBOOLE_1:63;
not ex n being Nat st for m being Nat st
n<=m holds |.s1.m-(lim s1).| < r
proof
given n being Nat such that
A14: for m being Nat st n<=m holds |.s1.m-(lim s1 ).| < r;
set m = n + 1;
reconsider ls = lim s1 as Element of REAL by XREAL_0:def 1;
|.s1.m-(ls).| < r by A14,NAT_1:11;
then real_dist.(s1.m,ls) < r by METRIC_1:def 12;
then
A15: real_dist.(ls,s1.m) < r by METRIC_1:9;
reconsider y = s1.m as Element of RealSpace by A9,TOPMETR:17;
A16: s1.m in rng s1 by FUNCT_2:4;
dist(x,y) = (the distance of RealSpace).(x,y) by METRIC_1:def 1;
then y in Ball(x,r) by A12,A15,METRIC_1:def 13;
then y in Ball(x,r) /\ (rng s1) by A16,XBOOLE_0:def 4;
hence thesis by A13,XBOOLE_0:def 7;
end;
hence thesis by A5,A10,SEQ_2:def 7;
end;
end;
hence thesis by RCOMP_1:def 4;
end;
case
A17: [#](P) = {};
for s1 being Real_Sequence st (rng s1) c= [#](P) & s1 is convergent
holds lim s1 in [#](P)
proof
let s1 be Real_Sequence;
assume that
A18: (rng s1) c= [#](P) and
s1 is convergent;
0 in NAT;
hence thesis by A17,A18,FUNCT_2:4;
end;
hence thesis by RCOMP_1:def 4;
end;
end;
hence thesis;
end;
theorem Th13:
for P being Subset of R^1 holds P is compact implies [#](P) is compact
proof
let P be Subset of R^1;
assume
A1: P is compact;
now
per cases;
case
[#](P) <> {};
[#](P) is real-bounded by A1,Th11;
hence thesis by A1,Th12,RCOMP_1:11;
end;
case
A2: [#](P) = {};
assume not [#](P) is compact;
then
A3: ex s1 being Real_Sequence st (rng s1) c= [#](P) & not(ex s2 being
Real_Sequence st s2 is subsequence of s1 & s2 is convergent & (lim s2) in [#](P
)) by RCOMP_1:def 3;
0 in NAT;
hence thesis by A2,A3,FUNCT_2:4;
end;
end;
hence thesis;
end;
Lm1: for T being non empty TopSpace holds for f being Function of T,R^1 holds
for P being Subset of T holds P <> {} & P is compact & f is continuous implies
ex x1,x2 being Point of T st x1 in P & x2 in P & f.x1 = upper_bound [#](f.:P) &
f.x2 = lower_bound [#](f.:P)
proof
let T be non empty TopSpace;
let f be Function of T,R^1;
let P be Subset of T;
assume that
A1: P <> {} and
A2: P is compact & f is continuous;
A3: [#](f.:P) <> {}
proof
consider x being object such that
A4: x in P by A1,XBOOLE_0:def 1;
dom f = the carrier of T by FUNCT_2:def 1;
then f.x in f.:P by A4,FUNCT_1:def 6;
hence thesis;
end;
consider y1,y2 being Real such that
A5: y1 = upper_bound [#](f.:P) and
A6: y2 = lower_bound [#](f.:P);
A7: [#](f.:P) is compact by A2,Th8,Th13;
then y1 in [#](f.:P) by A3,A5,RCOMP_1:14;
then consider x1 being object such that
A8: x1 in dom f and
A9: x1 in P & y1 = f.x1 by FUNCT_1:def 6;
y2 in [#](f.:P) by A3,A6,A7,RCOMP_1:14;
then consider x2 being object such that
A10: x2 in dom f and
A11: x2 in P & y2 = f.x2 by FUNCT_1:def 6;
reconsider x1,x2 as Point of T by A8,A10;
take x1;
take x2;
thus thesis by A5,A6,A9,A11;
end;
definition
let P be Subset of R^1;
func upper_bound(P) -> Real equals
upper_bound([#](P));
correctness;
func lower_bound(P) -> Real equals
lower_bound([#](P));
correctness;
end;
::$N Extreme value theorem#Generalization to arbitrary topological spaces
theorem Th14:
for T being non empty TopSpace holds for f being Function of T,
R^1 holds for P being Subset of T holds P <> {} & P is compact & f is
continuous implies ex x1 being Point of T st x1 in P & f.x1 = upper_bound(f.:P)
proof
let T be non empty TopSpace;
let f be Function of T,R^1;
let P be Subset of T;
assume P <> {} & P is compact & f is continuous;
then consider x1,x2 being Point of T such that
A1: x1 in P and
x2 in P and
A2: f.x1 = upper_bound [#](f.:P) and
f.x2 = lower_bound [#](f.:P) by Lm1;
take x1;
thus thesis by A1,A2;
end;
::$N Extreme value theorem#Generalization to arbitrary topological spaces
theorem Th15:
for T being non empty TopSpace holds for f being Function of T,
R^1 holds for P being Subset of T holds P <> {} & P is compact & f is
continuous implies ex x2 being Point of T st x2 in P & f.x2 = lower_bound(f.:P)
proof
let T be non empty TopSpace;
let f be Function of T,R^1;
let P be Subset of T;
assume P <> {} & P is compact & f is continuous;
then consider x1,x2 being Point of T such that
x1 in P and
A1: x2 in P and
f.x1 = upper_bound [#](f.:P) and
A2: f.x2 = lower_bound [#](f.:P) by Lm1;
take x2;
thus thesis by A1,A2;
end;
begin
::
:: The measure of the distance between compact sets
::
definition
let M be non empty MetrSpace;
let x be Point of M;
func dist(x) -> Function of TopSpaceMetr(M),R^1 means
:Def4:
for y being Point of M holds it.y = dist(y,x);
existence
proof
defpred EF[Element of M,Element of R^1] means for s being Element of M
holds for t being Element of R^1 holds ($1 = s & $2 = t implies t = dist(s,x));
A1: for s being Element of M ex t being Element of R^1 st EF[s,t]
proof
let s be Element of M;
dist(s,x) in REAL by XREAL_0:def 1;
then reconsider t = dist(s,x) as Element of R^1 by TOPMETR:17;
take t;
thus thesis;
end;
consider F being Function of the carrier of M,the carrier of R^1 such that
A2: for x being Element of M holds EF[x,F.x] from FUNCT_2:sch 3(A1);
A3: for y being Point of M holds F.y = dist(y,x) by A2;
TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#) by
PCOMPS_1:def 5;
then reconsider F as Function of TopSpaceMetr(M),R^1;
take F;
thus thesis by A3;
end;
uniqueness
proof
let F1,F2 be Function of TopSpaceMetr(M),R^1;
assume
A4: for y being Point of M holds F1.y = dist(y,x);
assume
A5: for y being Point of M holds F2.y = dist(y,x);
for y being object st y in the carrier of TopSpaceMetr(M)
holds F1.y = F2 .y
proof
let y be object;
A6: TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#)
by PCOMPS_1:def 5;
assume y in the carrier of TopSpaceMetr(M);
then reconsider y as Point of M by A6;
F1.y = dist(y,x) by A4
.= F2.y by A5;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th16:
for M being non empty MetrSpace holds for x being Point of M
holds dist(x) is continuous
proof
let M be non empty MetrSpace;
let x be Point of M;
A1: for P being Subset of R^1 st P is open holds (dist x)"P is open
proof
let P be Subset of R^1;
assume
A2: P is open;
for p being Point of M st p in (dist(x))"P ex r being Real st r
>0 & Ball(p,r) c= (dist(x))"P
proof
let p be Point of M;
dist(p,x) in REAL by XREAL_0:def 1;
then consider y being Point of RealSpace such that
A3: y = dist(p,x) by METRIC_1:def 13;
assume p in (dist(x))"P;
then
A4: (dist(x)).p in P by FUNCT_1:def 7;
reconsider P as Subset of TopSpaceMetr(RealSpace) by TOPMETR:def 6;
y in P by A4,A3,Def4;
then consider r being Real such that
A5: r>0 and
A6: Ball(y,r) c= P by A2,TOPMETR:15,def 6;
reconsider r as Real;
take r;
Ball(p,r) c= (dist(x))"P
proof
let z be object;
assume
A7: z in Ball(p,r);
then reconsider z as Point of M;
dist(z,x) in REAL by XREAL_0:def 1;
then consider q being Point of RealSpace such that
A8: q = dist(z,x) by METRIC_1:def 13;
dist(p,z) < r by A7,METRIC_1:11;
then |.dist(p,x)-dist(z,x).|+dist(p,z) < r+dist(p,z) by METRIC_6:1
,XREAL_1:8;
then |.dist(p,x)-dist(z,x).| < r by XREAL_1:6;
then dist(y,q) < r by A3,A8,TOPMETR:11;
then q in Ball(y,r) by METRIC_1:11;
then q in P by A6;
then
A9: (dist(x)).z in P by A8,Def4;
dom (dist(x)) = the carrier of TopSpaceMetr(M) by FUNCT_2:def 1;
then dom (dist(x)) = the carrier of M by TOPMETR:12;
hence thesis by A9,FUNCT_1:def 7;
end;
hence thesis by A5;
end;
hence (dist(x))"P is open by TOPMETR:15;
end;
[#]R^1 <> {};
hence thesis by A1,TOPS_2:43;
end;
theorem
for M being non empty MetrSpace holds for x being Point of M holds for
P being Subset of TopSpaceMetr(M) holds P <> {} & P is compact implies ex x1
being Point of TopSpaceMetr(M) st x1 in P & (dist(x)).x1 = upper_bound((dist(x)
).:P) by Th14,Th16;
theorem
for M being non empty MetrSpace holds for x being Point of M holds for
P being Subset of TopSpaceMetr(M) holds P <> {} & P is compact implies ex x2
being Point of TopSpaceMetr(M) st x2 in P & (dist(x)).x2 = lower_bound((dist(x)
).:P) by Th15,Th16;
definition
let M be non empty MetrSpace;
let P be Subset of TopSpaceMetr(M);
func dist_max(P) -> Function of TopSpaceMetr(M),R^1 means
:Def5:
for x being Point of M holds it.x = upper_bound((dist(x)).:P);
existence
proof
defpred EF[Element of M,Element of R^1] means for s being Element of M
holds for t being Element of R^1 holds ($1 = s & $2 = t implies t = upper_bound
((dist(s)).:P));
A1: for s being Element of M ex t being Element of R^1 st EF[s,t]
proof
let s be Element of M;
set t = upper_bound((dist(s)).:P);
t in REAL by XREAL_0:def 1;
then reconsider t as Element of R^1 by TOPMETR:17;
take t;
thus thesis;
end;
consider F being Function of the carrier of M,the carrier of R^1 such that
A2: for x being Element of M holds EF[x,F.x] from FUNCT_2:sch 3(A1);
A3: for y being Point of M holds F.y = upper_bound((dist(y)).:P) by A2;
TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#) by
PCOMPS_1:def 5;
then reconsider F as Function of TopSpaceMetr(M),R^1;
take F;
thus thesis by A3;
end;
uniqueness
proof
let F1,F2 be Function of TopSpaceMetr(M),R^1;
assume
A4: for y being Point of M holds F1.y = upper_bound((dist(y)).:P);
assume
A5: for y being Point of M holds F2.y = upper_bound((dist(y)).:P);
for y being object st y in the carrier of TopSpaceMetr(M)
holds F1.y = F2 .y
proof
let y be object;
A6: TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#)
by PCOMPS_1:def 5;
assume y in the carrier of TopSpaceMetr(M);
then reconsider y as Point of M by A6;
F1.y = upper_bound((dist(y)).:P) by A4
.= F2.y by A5;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
func dist_min(P) -> Function of TopSpaceMetr(M),R^1 means
:Def6:
for x being Point of M holds it.x = lower_bound((dist(x)).:P);
existence
proof
defpred EF[Element of M,Element of R^1] means for s being Element of M
holds for t being Element of R^1 holds ($1 = s & $2 = t implies t = lower_bound
((dist(s)).:P));
A7: for s being Element of M ex t being Element of R^1 st EF[s,t]
proof
let s be Element of M;
set t = lower_bound((dist(s)).:P);
t in REAL by XREAL_0:def 1;
then reconsider t as Element of R^1 by TOPMETR:17;
take t;
thus thesis;
end;
consider F being Function of the carrier of M,the carrier of R^1 such that
A8: for x being Element of M holds EF[x,F.x] from FUNCT_2:sch 3(A7);
A9: for y being Point of M holds F.y = lower_bound((dist(y)).:P) by A8;
TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#) by
PCOMPS_1:def 5;
then reconsider F as Function of TopSpaceMetr(M),R^1;
take F;
thus thesis by A9;
end;
uniqueness
proof
let F1,F2 be Function of TopSpaceMetr(M),R^1;
assume
A10: for y being Point of M holds F1.y = lower_bound((dist(y)).:P);
assume
A11: for y being Point of M holds F2.y = lower_bound((dist(y)).:P);
for y being object st y in the carrier of TopSpaceMetr(M)
holds F1.y = F2.y
proof
let y be object;
A12: TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#)
by PCOMPS_1:def 5;
assume y in the carrier of TopSpaceMetr(M);
then reconsider y as Point of M by A12;
F1.y = lower_bound((dist(y)).:P) by A10
.= F2.y by A11;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th19:
for M being non empty MetrSpace holds for P being Subset of
TopSpaceMetr(M) st P is compact for p1,p2 being Point of M holds p1 in P
implies dist(p1,p2) <= upper_bound((dist(p2)).:P) & lower_bound((dist(p2)).:P)
<= dist(p1,p2)
proof
let M be non empty MetrSpace;
let P be Subset of TopSpaceMetr(M);
assume
A1: P is compact;
let p1,p2 be Point of M;
dist(p2) is continuous by Th16;
then [#]((dist(p2)).:P) is real-bounded by A1,Th8,Th11;
then
A2: [#]((dist(p2)).:P) is bounded_above & [#]((dist(p2)).:P) is
bounded_below;
assume
A3: p1 in P;
dist(p1,p2) = (dist(p2)).p1 & dom (dist(p2)) = the carrier of
TopSpaceMetr(M ) by Def4,FUNCT_2:def 1;
then dist(p1,p2) in [#]((dist(p2)).:P) by A3,FUNCT_1:def 6;
hence thesis by A2,SEQ_4:def 1,def 2;
end;
theorem Th20:
for M being non empty MetrSpace holds for P being Subset of
TopSpaceMetr(M) st P <> {} & P is compact holds for p1,p2 being Point of M
holds |.upper_bound((dist(p1)).:P) - upper_bound((dist(p2)).:P).| <= dist(p1,
p2)
proof
let M be non empty MetrSpace;
let P be Subset of TopSpaceMetr(M);
assume that
A1: P <> {} and
A2: P is compact;
let p1,p2 be Point of M;
consider x1 being Point of TopSpaceMetr(M) such that
A3: x1 in P and
A4: (dist(p1)).x1 = upper_bound((dist(p1)).:P) by A1,A2,Th14,Th16;
A5: TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#) by
PCOMPS_1:def 5;
then reconsider x1 as Point of M;
consider x2 being Point of TopSpaceMetr(M) such that
A6: x2 in P and
A7: (dist(p2)).x2 = upper_bound((dist(p2)).:P) by A1,A2,Th14,Th16;
reconsider x2 as Point of M by A5;
A8: dist(x2,p2) = upper_bound((dist(p2)).:P) by A7,Def4;
(dist(p1)).x1 = dist(x1,p1) by Def4;
then dist(x2,p2) <= dist(x2,p1) + dist(p1,p2) & dist(x2,p1) <= dist(x1,p1)
by A2,A4,A6,Th19,METRIC_1:4;
then
dist(x2,p2) - dist(x1,p1) <= dist(x2,p1) + dist(p1,p2) - dist(x2,p1) by
XREAL_1:13;
then
A9: -dist(p1,p2) <= -(dist(x2,p2) - dist(x1,p1)) by XREAL_1:24;
(dist(p2)).x2 = dist(x2,p2) by Def4;
then dist(x1,p1) <= dist(x1,p2) + dist(p2,p1) & dist(x1,p2) <= dist(x2,p2)
by A2,A3,A7,Th19,METRIC_1:4;
then
A10: dist(x1,p1) - dist(x2,p2) <= dist(x1,p2) + dist(p1,p2) - dist(x1,p2) by
XREAL_1:13;
dist(x1,p1) = upper_bound((dist(p1)).:P) by A4,Def4;
hence thesis by A8,A10,A9,ABSVALUE:5;
end;
theorem
for M being non empty MetrSpace holds for P being Subset of
TopSpaceMetr(M) st P <> {} & P is compact holds for p1,p2 being Point of M
holds for x1,x2 being Real holds x1 = (dist_max(P)).p1 & x2 = (dist_max(P)).p2
implies |.x1 - x2.| <= dist(p1,p2)
proof
let M be non empty MetrSpace;
let P be Subset of TopSpaceMetr(M);
assume
A1: P <> {} & P is compact;
let p1,p2 be Point of M;
let x1,x2 be Real;
assume
A2: x1 = (dist_max(P)).p1 & x2 = (dist_max(P)).p2;
(dist_max(P)).p1 = upper_bound((dist(p1)).:P) & (dist_max(P)).p2 =
upper_bound((dist(p2)).:P) by Def5;
hence thesis by A1,A2,Th20;
end;
theorem Th22:
for M being non empty MetrSpace holds for P being Subset of
TopSpaceMetr(M) st P <> {} & P is compact holds for p1,p2 being Point of M
holds |.lower_bound((dist(p1)).:P) - lower_bound((dist(p2)).:P).| <= dist(p1,
p2)
proof
let M be non empty MetrSpace;
let P be Subset of TopSpaceMetr(M);
assume that
A1: P <> {} and
A2: P is compact;
let p1,p2 be Point of M;
consider x1 being Point of TopSpaceMetr(M) such that
A3: x1 in P and
A4: (dist(p1)).x1 = lower_bound((dist(p1)).:P) by A1,A2,Th15,Th16;
A5: TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#) by
PCOMPS_1:def 5;
then reconsider x1 as Point of M;
consider x2 being Point of TopSpaceMetr(M) such that
A6: x2 in P and
A7: (dist(p2)).x2 = lower_bound((dist(p2)).:P) by A1,A2,Th15,Th16;
reconsider x2 as Point of M by A5;
A8: dist(x2,p2) = lower_bound((dist(p2)).:P) by A7,Def4;
(dist(p2)).x2 = dist(x2,p2) by Def4;
then dist(x1,p2) <= dist(x1,p1) + dist(p1,p2) & dist(x2,p2) <= dist(x1,p2)
by A2,A3,A7,Th19,METRIC_1:4;
then dist(x2,p2) <= dist(x1,p1) + dist(p1,p2) by XXREAL_0:2;
then dist(x2,p2) - dist(x1,p1) <= dist(p1,p2) by XREAL_1:20;
then
A9: -dist(p1,p2) <= -(dist(x2,p2) - dist(x1,p1)) by XREAL_1:24;
(dist(p1)).x1 = dist(x1,p1) by Def4;
then dist(x2,p1) <= dist(x2,p2) + dist(p2,p1) & dist(x1,p1) <= dist(x2,p1)
by A2,A4,A6,Th19,METRIC_1:4;
then dist(x1,p1) <= dist(x2,p2) + dist(p1,p2) by XXREAL_0:2;
then
A10: dist(x1,p1) - dist(x2,p2) <= dist(p1,p2) by XREAL_1:20;
dist(x1,p1) = lower_bound((dist(p1)).:P) by A4,Def4;
hence thesis by A8,A10,A9,ABSVALUE:5;
end;
theorem
for M being non empty MetrSpace holds for P being Subset of
TopSpaceMetr(M) st P <> {} & P is compact holds for p1,p2 being Point of M
holds for x1,x2 being Real holds x1 = (dist_min(P)).p1 & x2 = (dist_min(P)).p2
implies |.x1 - x2.| <= dist(p1,p2)
proof
let M be non empty MetrSpace;
let P be Subset of TopSpaceMetr(M);
assume
A1: P <> {} & P is compact;
let p1,p2 be Point of M;
let x1,x2 be Real;
assume
A2: x1 = (dist_min(P)).p1 & x2 = (dist_min(P)).p2;
(dist_min(P)).p1 = lower_bound((dist(p1)).:P) & (dist_min(P)).p2 =
lower_bound((dist(p2)).:P) by Def6;
hence thesis by A1,A2,Th22;
end;
Lm2: [#]R^1 <> {};
theorem Th24:
for M being non empty MetrSpace holds for X being Subset of
TopSpaceMetr(M) st X <> {} & X is compact holds dist_max(X) is continuous
proof
let M be non empty MetrSpace;
let X be Subset of TopSpaceMetr(M);
assume
A1: X <> {} & X is compact;
for P being Subset of R^1 st P is open holds (dist_max(X))"P is open
proof
let P be Subset of R^1;
assume
A2: P is open;
for p being Point of M st p in (dist_max(X))"P ex r being Real
st r>0 & Ball(p,r) c= (dist_max(X))"P
proof
let p be Point of M;
set y = upper_bound((dist(p)).:(X));
y in REAL by XREAL_0:def 1;
then reconsider y as Point of RealSpace by METRIC_1:def 13;
assume p in (dist_max(X))"P;
then
A3: (dist_max(X)).p in P by FUNCT_1:def 7;
reconsider P as Subset of TopSpaceMetr(RealSpace) by TOPMETR:def 6;
y in P by A3,Def5;
then consider r being Real such that
A4: r>0 and
A5: Ball(y,r) c= P by A2,TOPMETR:15,def 6;
reconsider r as Real;
take r;
Ball(p,r) c= (dist_max(X))"P
proof
let z be object;
assume
A6: z in Ball(p,r);
then reconsider z as Point of M;
set q = upper_bound((dist(z)).:(X));
q in REAL by XREAL_0:def 1;
then reconsider q as Point of RealSpace by METRIC_1:def 13;
dist(p,z) < r by A6,METRIC_1:11;
then |.upper_bound((dist(p)).:(X)) - upper_bound((dist(z)).:(X)).|+
dist(p,z) < r+dist(p,z) by A1,Th20,XREAL_1:8;
then |.upper_bound((dist(p)).:(X)) - upper_bound((dist(z)).:(X)).| <
r by XREAL_1:6;
then dist(y,q) < r by TOPMETR:11;
then
A7: q in Ball(y,r) by METRIC_1:11;
dom (dist_max(X)) = the carrier of TopSpaceMetr(M) by FUNCT_2:def 1;
then
A8: dom (dist_max(X)) = the carrier of M by TOPMETR:12;
q = (dist_max(X)).z by Def5;
hence thesis by A5,A7,A8,FUNCT_1:def 7;
end;
hence thesis by A4;
end;
hence thesis by TOPMETR:15;
end;
hence thesis by Lm2,TOPS_2:43;
end;
theorem
for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies
ex x1 being Point of TopSpaceMetr(M) st x1 in Q & (dist_max(P)).x1 =
upper_bound((dist_max(P)).:Q) by Th14,Th24;
theorem
for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies
ex x2 being Point of TopSpaceMetr(M) st x2 in Q & (dist_max(P)).x2 =
lower_bound((dist_max(P)).:Q) by Th15,Th24;
theorem Th27:
for M being non empty MetrSpace holds for X being Subset of
TopSpaceMetr(M) st X <> {} & X is compact holds dist_min(X) is continuous
proof
let M be non empty MetrSpace;
let X be Subset of TopSpaceMetr(M);
assume
A1: X <> {} & X is compact;
for P being Subset of R^1 st P is open holds (dist_min(X))"P is open
proof
let P be Subset of R^1;
assume
A2: P is open;
for p being Point of M st p in (dist_min(X))"P ex r being Real
st r>0 & Ball(p,r) c= (dist_min(X))"P
proof
let p be Point of M;
assume
A3: p in (dist_min(X))"P;
ex r being Real st r>0 & Ball(p,r) c= (dist_min(X))"P
proof
A4: (dist_min(X)).p in P by A3,FUNCT_1:def 7;
reconsider P as Subset of TopSpaceMetr(RealSpace) by TOPMETR:def 6;
set y = lower_bound((dist(p)).:(X));
y in REAL by XREAL_0:def 1;
then reconsider y as Point of RealSpace by METRIC_1:def 13;
y in P by A4,Def6;
then consider r being Real such that
A5: r>0 and
A6: Ball(y,r) c= P by A2,TOPMETR:15,def 6;
reconsider r as Real;
take r;
Ball(p,r) c= (dist_min(X))"P
proof
let z be object;
assume
A7: z in Ball(p,r);
then reconsider z as Point of M;
set q = lower_bound((dist(z)).:(X));
q in REAL by XREAL_0:def 1;
then reconsider q as Point of RealSpace by METRIC_1:def 13;
dist(p,z) < r by A7,METRIC_1:11;
then
|.lower_bound((dist(p)).:(X)) - lower_bound((dist(z)).:(X)).|+
dist(p,z) < r+dist(p,z) by A1,Th22,XREAL_1:8;
then |.lower_bound((dist(p)).:(X)) - lower_bound((dist(z)).:(X)).|
< r by XREAL_1:6;
then dist(y,q) < r by TOPMETR:11;
then
A8: q in Ball(y,r) by METRIC_1:11;
dom (dist_min(X)) = the carrier of TopSpaceMetr(M) by FUNCT_2:def 1;
then
A9: dom (dist_min(X)) = the carrier of M by TOPMETR:12;
q = (dist_min(X)).z by Def6;
hence thesis by A6,A8,A9,FUNCT_1:def 7;
end;
hence thesis by A5;
end;
hence thesis;
end;
hence (dist_min(X))"P is open by TOPMETR:15;
end;
hence thesis by Lm2,TOPS_2:43;
end;
theorem
for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies
ex x1 being Point of TopSpaceMetr(M) st x1 in Q & (dist_min(P)).x1 =
upper_bound((dist_min(P)).:Q) by Th14,Th27;
theorem
for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies
ex x2 being Point of TopSpaceMetr(M) st x2 in Q & (dist_min(P)).x2 =
lower_bound((dist_min(P)).:Q) by Th15,Th27;
definition
let M be non empty MetrSpace;
let P,Q be Subset of TopSpaceMetr(M);
func min_dist_min(P,Q) -> Real equals
lower_bound((dist_min(P)).:Q);
correctness;
func max_dist_min(P,Q) -> Real equals
upper_bound((dist_min(P)).:Q);
correctness;
func min_dist_max(P,Q) -> Real equals
lower_bound((dist_max(P)).:Q);
correctness;
func max_dist_max(P,Q) -> Real equals
upper_bound((dist_max(P)).:Q);
correctness;
end;
theorem
for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,
x2 being Point of M st x1 in P & x2 in Q & dist(x1,x2) = min_dist_min(P,Q)
proof
let M be non empty MetrSpace;
let P,Q be Subset of TopSpaceMetr(M);
assume that
A1: P <> {} & P is compact and
A2: Q <> {} & Q is compact;
consider x2 being Point of TopSpaceMetr(M) such that
A3: x2 in Q and
A4: (dist_min(P)).x2 = lower_bound((dist_min(P)).:Q) by A1,A2,Th15,Th27;
A5: TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#) by
PCOMPS_1:def 5;
then reconsider x2 as Point of M;
consider x1 being Point of TopSpaceMetr(M) such that
A6: x1 in P and
A7: (dist(x2)).x1 = lower_bound((dist(x2)).:P) by A1,Th15,Th16;
reconsider x1 as Point of M by A5;
take x1;
take x2;
dist(x1,x2) = (dist(x2)).x1 by Def4
.= lower_bound((dist_min(P)).:Q) by A4,A7,Def6;
hence thesis by A3,A6;
end;
theorem
for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,
x2 being Point of M st x1 in P & x2 in Q & dist(x1,x2) = min_dist_max(P,Q)
proof
let M be non empty MetrSpace;
let P,Q be Subset of TopSpaceMetr(M);
assume that
A1: P <> {} & P is compact and
A2: Q <> {} & Q is compact;
consider x2 being Point of TopSpaceMetr(M) such that
A3: x2 in Q and
A4: (dist_max(P)).x2 = lower_bound((dist_max(P)).:Q) by A1,A2,Th15,Th24;
A5: TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#) by
PCOMPS_1:def 5;
then reconsider x2 as Point of M;
consider x1 being Point of TopSpaceMetr(M) such that
A6: x1 in P and
A7: (dist(x2)).x1 = upper_bound((dist(x2)).:P) by A1,Th14,Th16;
reconsider x1 as Point of M by A5;
take x1;
take x2;
dist(x1,x2) = (dist(x2)).x1 by Def4
.= lower_bound((dist_max(P)).:Q) by A4,A7,Def5;
hence thesis by A3,A6;
end;
theorem
for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,
x2 being Point of M st x1 in P & x2 in Q & dist(x1,x2) = max_dist_min(P,Q)
proof
let M be non empty MetrSpace;
let P,Q be Subset of TopSpaceMetr(M);
assume that
A1: P <> {} & P is compact and
A2: Q <> {} & Q is compact;
consider x2 being Point of TopSpaceMetr(M) such that
A3: x2 in Q and
A4: (dist_min(P)).x2 = upper_bound((dist_min(P)).:Q) by A1,A2,Th14,Th27;
A5: TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#) by
PCOMPS_1:def 5;
then reconsider x2 as Point of M;
consider x1 being Point of TopSpaceMetr(M) such that
A6: x1 in P and
A7: (dist(x2)).x1 = lower_bound((dist(x2)).:P) by A1,Th15,Th16;
reconsider x1 as Point of M by A5;
take x1;
take x2;
dist(x1,x2) = (dist(x2)).x1 by Def4
.= upper_bound((dist_min(P)).:Q) by A4,A7,Def6;
hence thesis by A3,A6;
end;
theorem
for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,
x2 being Point of M st x1 in P & x2 in Q & dist(x1,x2) = max_dist_max(P,Q)
proof
let M be non empty MetrSpace;
let P,Q be Subset of TopSpaceMetr(M);
assume that
A1: P <> {} & P is compact and
A2: Q <> {} & Q is compact;
consider x2 being Point of TopSpaceMetr(M) such that
A3: x2 in Q and
A4: (dist_max(P)).x2 = upper_bound((dist_max(P)).:Q) by A1,A2,Th14,Th24;
A5: TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#) by
PCOMPS_1:def 5;
then reconsider x2 as Point of M;
consider x1 being Point of TopSpaceMetr(M) such that
A6: x1 in P and
A7: (dist(x2)).x1 = upper_bound((dist(x2)).:P) by A1,Th14,Th16;
reconsider x1 as Point of M by A5;
take x1;
take x2;
dist(x1,x2) = (dist(x2)).x1 by Def4
.= upper_bound((dist_max(P)).:Q) by A4,A7,Def5;
hence thesis by A3,A6;
end;
theorem
for M being non empty MetrSpace holds for P,Q being Subset of
TopSpaceMetr(M) st P is compact & Q is compact holds for x1,x2 being Point of M
st x1 in P & x2 in Q holds min_dist_min(P,Q) <= dist(x1,x2) & dist(x1,x2) <=
max_dist_max(P,Q)
proof
let M be non empty MetrSpace;
let P,Q be Subset of TopSpaceMetr(M);
assume that
A1: P is compact and
A2: Q is compact;
let x1,x2 be Point of M;
assume that
A3: x1 in P and
A4: x2 in Q;
dist_max(P) is continuous by A1,A3,Th24;
then [#]((dist_max(P)).:Q) is real-bounded by A2,Th8,Th11;
then
A5: [#]((dist_max(P)).:Q) is bounded_above;
x2 in the carrier of M;
then x2 in the carrier of TopSpaceMetr(M) by TOPMETR:12;
then (dist_min(P)).x2 in the carrier of R^1 by FUNCT_2:5;
then consider z being Real such that
A6: z = (dist_min(P)).x2;
dist_min(P) is continuous by A1,A3,Th27;
then [#]((dist_min(P)).:Q) is real-bounded by A2,Th8,Th11;
then
A7: [#]((dist_min(P)).:Q) is bounded_below;
dom (dist_min(P)) = the carrier of TopSpaceMetr(M) by FUNCT_2:def 1;
then z in [#]((dist_min(P)).:Q) by A4,A6,FUNCT_1:def 6;
then
A8: lower_bound((dist_min(P)).:Q) <= z by A7,SEQ_4:def 2;
x2 in the carrier of M;
then x2 in the carrier of TopSpaceMetr(M) by TOPMETR:12;
then (dist_max(P)).x2 in the carrier of R^1 by FUNCT_2:5;
then consider y being Real such that
A9: y = (dist_max(P)).x2;
dom (dist_max(P)) = the carrier of TopSpaceMetr(M) by FUNCT_2:def 1;
then y in [#]((dist_max(P)).:Q) by A4,A9,FUNCT_1:def 6;
then
A10: y <= upper_bound((dist_max(P)).:Q) by A5,SEQ_4:def 1;
A11: lower_bound((dist(x2)).:P) = z by A6,Def6;
A12: upper_bound((dist(x2)).:P) = y by A9,Def5;
dist(x1,x2) <= upper_bound((dist(x2)).:P) & lower_bound((dist(x2)).:P)
<= dist(x1,x2) by A1,A3,Th19;
hence thesis by A12,A10,A11,A8,XXREAL_0:2;
end;
:: B i b l i o g r a p h y
:: J.Dieudonne, "Foundations of Modern Analysis",Academic Press, 1960.
:: J.L.Kelley, "General Topology", von Nostnend, 1955.
:: K.Yosida, "Functional Analysis", Springer Verlag, 1968.