:: The Theorem of Weierstrass
:: by J\'ozef Bia\las and Yatsuka Nakamura
::
:: Received July 10, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, 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;
begin
theorem :: WEIERSTR:1
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);
theorem :: WEIERSTR:2
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) );
theorem :: WEIERSTR:3
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);
theorem :: WEIERSTR:4
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;
theorem :: WEIERSTR:5
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;
theorem :: WEIERSTR:6
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
;
theorem :: WEIERSTR:7
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;
begin
::
:: The Weierstrass` theorem
::
theorem :: WEIERSTR:8
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;
theorem :: WEIERSTR:9
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;
theorem :: WEIERSTR:10
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;
definition
let P be Subset of R^1;
func [#](P) -> Subset of REAL equals
:: WEIERSTR:def 1
P;
end;
theorem :: WEIERSTR:11
for P being Subset of R^1 holds P is compact implies [#](P) is real-bounded;
theorem :: WEIERSTR:12
for P being Subset of R^1 holds P is compact implies [#](P) is closed;
theorem :: WEIERSTR:13
for P being Subset of R^1 holds P is compact implies [#](P) is compact;
definition
let P be Subset of R^1;
func upper_bound(P) -> Real equals
:: WEIERSTR:def 2
upper_bound([#](P));
func lower_bound(P) -> Real equals
:: WEIERSTR:def 3
lower_bound([#](P));
end;
::$N Extreme value theorem#Generalization to arbitrary topological spaces
theorem :: WEIERSTR:14
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)
;
::$N Extreme value theorem#Generalization to arbitrary topological spaces
theorem :: WEIERSTR:15
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)
;
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
:: WEIERSTR:def 4
for y being Point of M holds it.y = dist(y,x);
end;
theorem :: WEIERSTR:16
for M being non empty MetrSpace holds for x being Point of M
holds dist(x) is continuous;
theorem :: WEIERSTR:17
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);
theorem :: WEIERSTR:18
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);
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
:: WEIERSTR:def 5
for x being Point of M holds it.x = upper_bound((dist(x)).:P);
func dist_min(P) -> Function of TopSpaceMetr(M),R^1 means
:: WEIERSTR:def 6
for x being Point of M holds it.x = lower_bound((dist(x)).:P);
end;
theorem :: WEIERSTR:19
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);
theorem :: WEIERSTR:20
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);
theorem :: WEIERSTR:21
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);
theorem :: WEIERSTR:22
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);
theorem :: WEIERSTR:23
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);
theorem :: WEIERSTR:24
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;
theorem :: WEIERSTR:25
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);
theorem :: WEIERSTR:26
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);
theorem :: WEIERSTR:27
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;
theorem :: WEIERSTR:28
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);
theorem :: WEIERSTR:29
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);
definition
let M be non empty MetrSpace;
let P,Q be Subset of TopSpaceMetr(M);
func min_dist_min(P,Q) -> Real equals
:: WEIERSTR:def 7
lower_bound((dist_min(P)).:Q);
func max_dist_min(P,Q) -> Real equals
:: WEIERSTR:def 8
upper_bound((dist_min(P)).:Q);
func min_dist_max(P,Q) -> Real equals
:: WEIERSTR:def 9
lower_bound((dist_max(P)).:Q);
func max_dist_max(P,Q) -> Real equals
:: WEIERSTR:def 10
upper_bound((dist_max(P)).:Q);
end;
theorem :: WEIERSTR:30
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);
theorem :: WEIERSTR:31
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);
theorem :: WEIERSTR:32
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);
theorem :: WEIERSTR:33
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);
theorem :: WEIERSTR:34
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);
:: 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.