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

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

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)

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

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

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

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 )

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

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

theorem :: WEIERSTR:10

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;

correctness

coherence

upper_bound ([#] P) is Real;

;

correctness

coherence

lower_bound ([#] P) is Real;

;

end;
correctness

coherence

upper_bound ([#] P) is Real;

;

correctness

coherence

lower_bound ([#] P) is Real;

;

:: deftheorem defines upper_bound WEIERSTR:def 2 :

for P being Subset of R^1 holds upper_bound P = upper_bound ([#] P);

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

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

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

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

::

:: The measure of the distance between compact sets

::

definition

let M be non empty MetrSpace;

let x be Point of M;

ex b_{1} being Function of (TopSpaceMetr M),R^1 st

for y being Point of M holds b_{1} . y = dist (y,x)

for b_{1}, b_{2} being Function of (TopSpaceMetr M),R^1 st ( for y being Point of M holds b_{1} . y = dist (y,x) ) & ( for y being Point of M holds b_{2} . y = dist (y,x) ) holds

b_{1} = b_{2}

end;
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 for y being Point of M holds it . y = dist (y,x);

ex b

for y being Point of M holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines dist WEIERSTR:def 4 :

for M being non empty MetrSpace

for x being Point of M

for b_{3} being Function of (TopSpaceMetr M),R^1 holds

( b_{3} = dist x iff for y being Point of M holds b_{3} . y = dist (y,x) );

for M being non empty MetrSpace

for x being Point of M

for b

( b

theorem :: WEIERSTR:17

theorem :: WEIERSTR:18

definition

let M be non empty MetrSpace;

let P be Subset of (TopSpaceMetr M);

ex b_{1} being Function of (TopSpaceMetr M),R^1 st

for x being Point of M holds b_{1} . x = upper_bound ((dist x) .: P)

for b_{1}, b_{2} being Function of (TopSpaceMetr M),R^1 st ( for x being Point of M holds b_{1} . x = upper_bound ((dist x) .: P) ) & ( for x being Point of M holds b_{2} . x = upper_bound ((dist x) .: P) ) holds

b_{1} = b_{2}

ex b_{1} being Function of (TopSpaceMetr M),R^1 st

for x being Point of M holds b_{1} . x = lower_bound ((dist x) .: P)

for b_{1}, b_{2} being Function of (TopSpaceMetr M),R^1 st ( for x being Point of M holds b_{1} . x = lower_bound ((dist x) .: P) ) & ( for x being Point of M holds b_{2} . x = lower_bound ((dist x) .: P) ) holds

b_{1} = b_{2}

end;
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 for x being Point of M holds it . x = upper_bound ((dist x) .: P);

ex b

for x being Point of M holds b

proof end;

uniqueness for 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 for x being Point of M holds it . x = lower_bound ((dist x) .: P);

ex b

for x being Point of M holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines dist_max WEIERSTR:def 5 :

for M being non empty MetrSpace

for P being Subset of (TopSpaceMetr M)

for b_{3} being Function of (TopSpaceMetr M),R^1 holds

( b_{3} = dist_max P iff for x being Point of M holds b_{3} . x = upper_bound ((dist x) .: P) );

for M being non empty MetrSpace

for P being Subset of (TopSpaceMetr M)

for b

( b

:: deftheorem Def6 defines dist_min WEIERSTR:def 6 :

for M being non empty MetrSpace

for P being Subset of (TopSpaceMetr M)

for b_{3} being Function of (TopSpaceMetr M),R^1 holds

( b_{3} = dist_min P iff for x being Point of M holds b_{3} . x = lower_bound ((dist x) .: P) );

for M being non empty MetrSpace

for P being Subset of (TopSpaceMetr M)

for b

( b

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

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)

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)

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)

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)

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

for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds

dist_max X is continuous

proof end;

theorem :: WEIERSTR:25

theorem :: WEIERSTR:26

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

for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds

dist_min X is continuous

proof end;

theorem :: WEIERSTR:28

theorem :: WEIERSTR:29

definition

let M be non empty MetrSpace;

let P, Q be Subset of (TopSpaceMetr M);

correctness

coherence

lower_bound ((dist_min P) .: Q) is Real;

;

correctness

coherence

upper_bound ((dist_min P) .: Q) is Real;

;

correctness

coherence

lower_bound ((dist_max P) .: Q) is Real;

;

correctness

coherence

upper_bound ((dist_max P) .: Q) is Real;

;

end;
let P, Q be Subset of (TopSpaceMetr M);

correctness

coherence

lower_bound ((dist_min P) .: Q) is Real;

;

correctness

coherence

upper_bound ((dist_min P) .: Q) is Real;

;

correctness

coherence

lower_bound ((dist_max P) .: Q) is Real;

;

correctness

coherence

upper_bound ((dist_max P) .: Q) is Real;

;

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

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

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

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

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

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

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

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

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

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;

:: The Weierstrass` theorem

::