:: The Theorem of Weierstrass
:: by J\'ozef Bia\las and Yatsuka Nakamura
::
:: Received July 10, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

theorem Th1: :: WEIERSTR:1
for M being MetrSpace
for x1, x2 being Point of M
for r1, r2 being Real ex x being Point of M ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r)
proofend;

theorem Th2: :: WEIERSTR:2
for M being MetrSpace
for n being Nat
for F being Subset-Family of M
for 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 ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
proofend;

theorem Th3: :: WEIERSTR:3
for M being MetrSpace
for F being Subset-Family of M st F is finite & F is being_ball-family holds
ex x being Point of M ex r being Real st union F c= Ball (x,r)
proofend;

theorem Th4: :: WEIERSTR:4
for T, S being non empty TopSpace
for f being Function of T,S
for B being Subset-Family of S st f is continuous & B is open holds
f " B is open
proofend;

theorem :: WEIERSTR:5
for T, S being non empty TopSpace
for f being Function of T,S
for Q being Subset-Family of S st Q is finite holds
f " Q is finite
proofend;

theorem :: WEIERSTR:6
for T, S being non empty TopSpace
for f being Function of T,S
for P being Subset-Family of T st P is finite holds
f .: P is finite
proofend;

theorem Th7: :: WEIERSTR:7
for T, S being non empty TopSpace
for f being Function of T,S
for P being Subset of T
for F being Subset-Family of S st ex B being Subset-Family of T st
( B c= f " F & B is Cover of P & B is finite ) holds
ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
proofend;

begin

::
:: The Weierstrass` theorem
::
theorem Th8: :: WEIERSTR:8
for T, S being non empty TopSpace
for f being Function of T,S
for P being Subset of T st P is compact & f is continuous holds
f .: P is compact
proofend;

theorem :: WEIERSTR:9
for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P is compact & f is continuous holds
f .: P is compact by Th8;

theorem :: WEIERSTR:10
for f being Function of (TOP-REAL 2),R^1
for P being Subset of (TOP-REAL 2) st P is compact & f is continuous holds
f .: P is compact by Th8;

definition
let P be Subset of R^1;
func [#] P ->  Subset of REAL equals :: WEIERSTR:def 1
P;
correctness
coherence
P is Subset of REAL;
by TOPMETR:17;
end;

:: deftheorem  defines [#] WEIERSTR:def_1_:_
 for P being Subset of R^1 holds [#] P = P;

theorem Th11: :: WEIERSTR:11
for P being Subset of R^1 st P is compact holds
[#] P is real-bounded
proofend;

theorem Th12: :: WEIERSTR:12
for P being Subset of R^1 st P is compact holds
[#] P is closed
proofend;

theorem Th13: :: WEIERSTR:13
for P being Subset of R^1 st P is compact holds
[#] P is compact
proofend;

Lm1:  for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P <> {} &amp; P is compact &amp; f is continuous holds
ex x1, x2 being Point of T st
( x1 in P &amp; x2 in P &amp; f . x1 = upper_bound ([#] (f .: P)) &amp; f . x2 = lower_bound ([#] (f .: P)) )
proofend;

definition
let P be Subset of R^1;
func upper_bound P ->  Real equals :: WEIERSTR:def 2
 upper_bound ([#] P);
correctness
coherence
upper_bound ([#] P) is Real;
;
func lower_bound P ->  Real equals :: WEIERSTR:def 3
 lower_bound ([#] P);
correctness
coherence
lower_bound ([#] P) is Real;
;
end;

:: deftheorem  defines upper_bound WEIERSTR:def_2_:_
 for P being Subset of R^1 holds upper_bound P = upper_bound ([#] P);

:: deftheorem  defines lower_bound WEIERSTR:def_3_:_
 for P being Subset of R^1 holds lower_bound P = lower_bound ([#] P);

theorem Th14: :: WEIERSTR:14
for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P <> {} &amp; P is compact &amp; f is continuous holds
ex x1 being Point of T st
( x1 in P &amp; f . x1 = upper_bound (f .: P) )
proofend;

:: [WP: ] Weierstrass_Theorem
theorem Th15: :: WEIERSTR:15
for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P <> {} &amp; P is compact &amp; f is continuous holds
ex x2 being Point of T st
( x2 in P &amp; f . x2 = lower_bound (f .: P) )
proofend;

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: :: WEIERSTR:def 4
 for y being Point of M holds it . y = dist (y,x);
existence
 ex b1 being Function of (TopSpaceMetr M),R^1 st
for y being Point of M holds b1 . y = dist (y,x)
proofend;
uniqueness
 for b1, b2 being Function of (TopSpaceMetr M),R^1 st ( for y being Point of M holds b1 . y = dist (y,x) ) &amp; ( for y being Point of M holds b2 . y = dist (y,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines dist WEIERSTR:def_4_:_
 for M being non empty MetrSpace
for x being Point of M
for b3 being Function of (TopSpaceMetr M),R^1 holds
( b3 = dist x iff for y being Point of M holds b3 . y = dist (y,x) );

theorem Th16: :: WEIERSTR:16
for M being non empty MetrSpace
for x being Point of M holds dist x is continuous
proofend;

theorem :: WEIERSTR:17
for M being non empty MetrSpace
for x being Point of M
for P being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact holds
ex x1 being Point of (TopSpaceMetr M) st
( x1 in P &amp; (dist x) . x1 = upper_bound ((dist x) .: P) ) by Th14, Th16;

theorem :: WEIERSTR:18
for M being non empty MetrSpace
for x being Point of M
for P being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact holds
ex x2 being Point of (TopSpaceMetr M) st
( x2 in P &amp; (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: :: WEIERSTR:def 5
 for x being Point of M holds it . x = upper_bound ((dist x) .: P);
existence
 ex b1 being Function of (TopSpaceMetr M),R^1 st
for x being Point of M holds b1 . x = upper_bound ((dist x) .: P)
proofend;
uniqueness
 for b1, b2 being Function of (TopSpaceMetr M),R^1 st ( for x being Point of M holds b1 . x = upper_bound ((dist x) .: P) ) &amp; ( for x being Point of M holds b2 . x = upper_bound ((dist x) .: P) ) holds
b1 = b2
proofend;
func dist_min P ->  Function of (TopSpaceMetr M),R^1 means :Def6: :: WEIERSTR:def 6
 for x being Point of M holds it . x = lower_bound ((dist x) .: P);
existence
 ex b1 being Function of (TopSpaceMetr M),R^1 st
for x being Point of M holds b1 . x = lower_bound ((dist x) .: P)
proofend;
uniqueness
 for b1, b2 being Function of (TopSpaceMetr M),R^1 st ( for x being Point of M holds b1 . x = lower_bound ((dist x) .: P) ) &amp; ( for x being Point of M holds b2 . x = lower_bound ((dist x) .: P) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines dist_max WEIERSTR:def_5_:_
 for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for b3 being Function of (TopSpaceMetr M),R^1 holds
( b3 = dist_max P iff for x being Point of M holds b3 . x = upper_bound ((dist x) .: P) );

:: deftheorem Def6 defines dist_min WEIERSTR:def_6_:_
 for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for b3 being Function of (TopSpaceMetr M),R^1 holds
( b3 = dist_min P iff for x being Point of M holds b3 . x = lower_bound ((dist x) .: P) );

theorem Th19: :: WEIERSTR:19
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P is compact holds
for p1, p2 being Point of M st p1 in P holds
( dist (p1,p2) <= upper_bound ((dist p2) .: P) &amp; lower_bound ((dist p2) .: P) <= dist (p1,p2) )
proofend;

theorem Th20: :: WEIERSTR:20
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact holds
for p1, p2 being Point of M holds abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2)
proofend;

theorem :: WEIERSTR:21
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact holds
for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_max P) . p1 &amp; x2 = (dist_max P) . p2 holds
abs (x1 - x2) <= dist (p1,p2)
proofend;

theorem Th22: :: WEIERSTR:22
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact holds
for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2)
proofend;

theorem :: WEIERSTR:23
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact holds
for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_min P) . p1 &amp; x2 = (dist_min P) . p2 holds
abs (x1 - x2) <= dist (p1,p2)
proofend;

Lm2:  [#] R^1 <> {}
;

theorem Th24: :: WEIERSTR:24
for M being non empty MetrSpace
for X being Subset of (TopSpaceMetr M) st X <> {} &amp; X is compact holds
dist_max X is continuous
proofend;

theorem :: WEIERSTR:25
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact &amp; Q <> {} &amp; Q is compact holds
ex x1 being Point of (TopSpaceMetr M) st
( x1 in Q &amp; (dist_max P) . x1 = upper_bound ((dist_max P) .: Q) ) by Th14, Th24;

theorem :: WEIERSTR:26
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact &amp; Q <> {} &amp; Q is compact holds
ex x2 being Point of (TopSpaceMetr M) st
( x2 in Q &amp; (dist_max P) . x2 = lower_bound ((dist_max P) .: Q) ) by Th15, Th24;

theorem Th27: :: WEIERSTR:27
for M being non empty MetrSpace
for X being Subset of (TopSpaceMetr M) st X <> {} &amp; X is compact holds
dist_min X is continuous
proofend;

theorem :: WEIERSTR:28
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact &amp; Q <> {} &amp; Q is compact holds
ex x1 being Point of (TopSpaceMetr M) st
( x1 in Q &amp; (dist_min P) . x1 = upper_bound ((dist_min P) .: Q) ) by Th14, Th27;

theorem :: WEIERSTR:29
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact &amp; Q <> {} &amp; Q is compact holds
ex x2 being Point of (TopSpaceMetr M) st
( x2 in Q &amp; (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 :: WEIERSTR:def 7
 lower_bound ((dist_min P) .: Q);
correctness
coherence
lower_bound ((dist_min P) .: Q) is Real;
;
func max_dist_min (P,Q) ->  Real equals :: WEIERSTR:def 8
 upper_bound ((dist_min P) .: Q);
correctness
coherence
upper_bound ((dist_min P) .: Q) is Real;
;
func min_dist_max (P,Q) ->  Real equals :: WEIERSTR:def 9
 lower_bound ((dist_max P) .: Q);
correctness
coherence
lower_bound ((dist_max P) .: Q) is Real;
;
func max_dist_max (P,Q) ->  Real equals :: WEIERSTR:def 10
 upper_bound ((dist_max P) .: Q);
correctness
coherence
upper_bound ((dist_max P) .: Q) is Real;
;
end;

:: deftheorem  defines min_dist_min WEIERSTR:def_7_:_
 for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds min_dist_min (P,Q) = lower_bound ((dist_min P) .: Q);

:: deftheorem  defines max_dist_min WEIERSTR:def_8_:_
 for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds max_dist_min (P,Q) = upper_bound ((dist_min P) .: Q);

:: deftheorem  defines min_dist_max WEIERSTR:def_9_:_
 for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds min_dist_max (P,Q) = lower_bound ((dist_max P) .: Q);

:: deftheorem  defines max_dist_max WEIERSTR:def_10_:_
 for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) holds max_dist_max (P,Q) = upper_bound ((dist_max P) .: Q);

theorem :: WEIERSTR:30
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact &amp; Q <> {} &amp; Q is compact holds
ex x1, x2 being Point of M st
( x1 in P &amp; x2 in Q &amp; dist (x1,x2) = min_dist_min (P,Q) )
proofend;

theorem :: WEIERSTR:31
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact &amp; Q <> {} &amp; Q is compact holds
ex x1, x2 being Point of M st
( x1 in P &amp; x2 in Q &amp; dist (x1,x2) = min_dist_max (P,Q) )
proofend;

theorem :: WEIERSTR:32
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact &amp; Q <> {} &amp; Q is compact holds
ex x1, x2 being Point of M st
( x1 in P &amp; x2 in Q &amp; dist (x1,x2) = max_dist_min (P,Q) )
proofend;

theorem :: WEIERSTR:33
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} &amp; P is compact &amp; Q <> {} &amp; Q is compact holds
ex x1, x2 being Point of M st
( x1 in P &amp; x2 in Q &amp; dist (x1,x2) = max_dist_max (P,Q) )
proofend;

theorem :: WEIERSTR:34
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P is compact &amp; Q is compact holds
for x1, x2 being Point of M st x1 in P &amp; x2 in Q holds
( min_dist_min (P,Q) <= dist (x1,x2) &amp; dist (x1,x2) <= max_dist_max (P,Q) )
proofend;