:: 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)
proof end;

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)) ) )
proof end;

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)
proof end;

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
proof end;

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
proof end;

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
proof end;

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 )
proof end;

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
proof end;

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
proof end;

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

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

Lm1: for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
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 end;

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 <> {} & P is compact & f is continuous holds
ex x1 being Point of T st
( x1 in P & f . x1 = upper_bound (f .: P) )
proof end;

:: 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 <> {} & P is compact & f is continuous holds
ex x2 being Point of T st
( x2 in P & f . x2 = lower_bound (f .: P) )
proof 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: :: 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)
proof end;
uniqueness
for b1, b2 being Function of (TopSpaceMetr M),R^1 st ( for y being Point of M holds b1 . y = dist (y,x) ) & ( for y being Point of M holds b2 . y = dist (y,x) ) holds
b1 = b2
proof end;
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
proof end;

theorem :: WEIERSTR:17
for M being non empty MetrSpace
for x being Point of M
for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
ex x1 being Point of (TopSpaceMetr M) st
( x1 in P & (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 <> {} & P is compact holds
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: :: 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)
proof end;
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) ) & ( for x being Point of M holds b2 . x = upper_bound ((dist x) .: P) ) holds
b1 = b2
proof end;
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)
proof end;
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) ) & ( for x being Point of M holds b2 . x = lower_bound ((dist x) .: P) ) holds
b1 = b2
proof end;
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) & lower_bound ((dist p2) .: P) <= dist (p1,p2) )
proof end;

theorem Th20: :: WEIERSTR:20
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} & 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)
proof end;

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

theorem Th22: :: WEIERSTR:22
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} & 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)
proof end;

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

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

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

theorem :: WEIERSTR:25
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
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 :: WEIERSTR:26
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
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: :: WEIERSTR:27
for M being non empty MetrSpace
for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds
dist_min X is continuous
proof end;

theorem :: WEIERSTR:28
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
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 :: WEIERSTR:29
for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
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 :: 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 <> {} & 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 end;

theorem :: WEIERSTR:31
for M being non empty MetrSpace
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 end;

theorem :: WEIERSTR:32
for M being non empty MetrSpace
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 end;

theorem :: WEIERSTR:33
for M being non empty MetrSpace
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 end;

theorem :: WEIERSTR:34
for M being non empty MetrSpace
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 end;