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

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;

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

:: Extreme value theorem#Generalization to arbitrary topological spaces

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;

:: Extreme value theorem#Generalization to arbitrary topological spaces

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;

::
:: 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 b₁ being Function of (TopSpaceMetr M),R^1 st
for y being Point of M holds b₁ . y = dist (y,x)

proof end;

uniqueness
for b₁, b₂ being Function of (TopSpaceMetr M),R^1 st ( for y being Point of M holds b₁ . y = dist (y,x) ) & ( for y being Point of M holds b₂ . y = dist (y,x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines dist WEIERSTR:def 4 :
for M being non empty MetrSpace
for x being Point of M
for b₃ being Function of (TopSpaceMetr M),R^1 holds
( b₃ = dist x iff for y being Point of M holds b₃ . 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 b₁ being Function of (TopSpaceMetr M),R^1 st
for x being Point of M holds b₁ . x = upper_bound ((dist x) .: P)

proof end;

uniqueness
for b₁, b₂ being Function of (TopSpaceMetr M),R^1 st ( for x being Point of M holds b₁ . x = upper_bound ((dist x) .: P) ) & ( for x being Point of M holds b₂ . x = upper_bound ((dist x) .: P) ) holds
b₁ = b₂

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 b₁ being Function of (TopSpaceMetr M),R^1 st
for x being Point of M holds b₁ . x = lower_bound ((dist x) .: P)

proof end;

uniqueness
for b₁, b₂ being Function of (TopSpaceMetr M),R^1 st ( for x being Point of M holds b₁ . x = lower_bound ((dist x) .: P) ) & ( for x being Point of M holds b₂ . x = lower_bound ((dist x) .: P) ) holds
b₁ = b₂

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 b₃ being Function of (TopSpaceMetr M),R^1 holds
( b₃ = dist_max P iff for x being Point of M holds b₃ . 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 b₃ being Function of (TopSpaceMetr M),R^1 holds
( b₃ = dist_min P iff for x being Point of M holds b₃ . 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 |.((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
|.(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 |.((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
|.(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;