:: The Theorem of Weierstrass
:: by J\'ozef Bia\las and Yatsuka Nakamura
::
:: Received July 10, 1995
:: Copyright (c) 1995 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 :: WEIERSTR:4

canceled;

theorem Th5: :: WEIERSTR:5

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:6

canceled;

theorem :: WEIERSTR:7

canceled;

theorem :: WEIERSTR:8

canceled;

theorem :: WEIERSTR:9

canceled;

theorem :: WEIERSTR:10

canceled;

theorem :: WEIERSTR:11

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:12

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 Th13: :: WEIERSTR:13

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

theorem Th14: :: WEIERSTR:14

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:15

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 Th14;

theorem :: WEIERSTR:16

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 Th14;

definition

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

end;

:: deftheorem WEIERSTR:def 1 :
canceled;

:: deftheorem WEIERSTR:def 2 :
canceled;

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

theorem Th17: :: WEIERSTR:17

for P being Subset of R^1 st P is compact holds
[#] P is bounded

proof end;

theorem Th18: :: WEIERSTR:18

for P being Subset of R^1 st P is compact holds
[#] P is closed

proof end;

theorem Th19: :: WEIERSTR:19

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 4
upper_bound ([#] P);
correctness
coherence
upper_bound ([#] P) is Real;
;
func lower_bound P -> Real equals :: WEIERSTR:def 5
lower_bound ([#] P);
correctness
coherence
lower_bound ([#] P) is Real;
;

end;

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

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

theorem Th20: :: WEIERSTR:20

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;

theorem Th21: :: WEIERSTR:21

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

definition

let M be non empty MetrSpace;
let x be Point of M;
func dist x -> Function of (TopSpaceMetr M),R^1 means :Def6: :: WEIERSTR:def 6
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 Def6 defines dist WEIERSTR:def 6 :
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 Th22: :: WEIERSTR:22

for M being non empty MetrSpace
for x being Point of M holds dist x is continuous

proof end;

theorem :: WEIERSTR:23

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 Th20, Th22;

theorem :: WEIERSTR:24

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 Th21, Th22;

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 :Def7: :: WEIERSTR:def 7
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 :Def8: :: WEIERSTR:def 8
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 Def7 defines dist_max WEIERSTR:def 7 :
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 Def8 defines dist_min WEIERSTR:def 8 :
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 Th25: :: WEIERSTR:25

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 Th26: :: WEIERSTR:26

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:27

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 Th28: :: WEIERSTR:28

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:29

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 Th30: :: WEIERSTR:30

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: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 being Point of (TopSpaceMetr M) st
( x1 in Q & (dist_max P) . x1 = upper_bound ((dist_max P) .: Q) ) by Th20, Th30;

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 x2 being Point of (TopSpaceMetr M) st
( x2 in Q & (dist_max P) . x2 = lower_bound ((dist_max P) .: Q) ) by Th21, Th30;

theorem Th33: :: WEIERSTR:33

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:34

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 Th20, Th33;

theorem :: WEIERSTR:35

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 Th21, Th33;

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 9
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 10
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 11
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 12
upper_bound ((dist_max P) .: Q);
correctness
coherence
upper_bound ((dist_max P) .: Q) is Real;
;

end;

:: deftheorem defines min_dist_min WEIERSTR:def 9 :
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 10 :
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 11 :
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 12 :
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:36

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:37

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:38

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:39

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:40

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;