:: WEIERSTR semantic presentation

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 finite & F is_ball-family & rng p = F & dom p = Seg (n + 1) holds
ex G being Subset-Family of M st
( G is finite & G is_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_ball-family holds
ex x being Point of M ex r being Real st union F c= Ball x,r

proof end;

definition

let T, S be non empty TopSpace;
let f be Function of T,S;
let G be Subset-Family of S;
func f " G -> Subset-Family of T means :Def1: :: WEIERSTR:def 1
for A being Subset of T holds
( A in it iff ex B being Subset of S st
( B in G & A = f " B ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines " WEIERSTR:def 1 :

theorem :: WEIERSTR:4

for T, S being non empty TopSpace
for f being Function of T,S
for A, B being Subset-Family of S st A c= B holds
f " A c= f " B

proof end;

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;

definition

let T, S be non empty TopSpace;
let f be Function of T,S;
let G be Subset-Family of T;
func f .: G -> Subset-Family of S means :Def2: :: WEIERSTR:def 2
for A being Subset of S holds
( A in it iff ex B being Subset of T st
( B in G & A = f .: B ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines .: WEIERSTR:def 2 :

theorem :: WEIERSTR:6

for T, S being non empty TopSpace
for f being Function of T,S
for A, B being Subset-Family of T st A c= B holds
f .: A c= f .: B

proof end;

theorem :: WEIERSTR:7

for T, S being non empty TopSpace
for f being Function of T,S
for B being Subset-Family of S
for P being Subset of S st f .: (f " B) is_a_cover_of P holds
B is_a_cover_of P

proof end;

theorem :: WEIERSTR:8

for T, S being non empty TopSpace
for f being Function of T,S
for B being Subset-Family of T
for P being Subset of T st B is_a_cover_of P holds
f " (f .: B) is_a_cover_of P

proof end;

theorem :: WEIERSTR:9

for T, S being non empty TopSpace
for f being Function of T,S
for Q being Subset-Family of S holds union (f .: (f " Q)) c= union Q

proof end;

theorem :: WEIERSTR:10

for T, S being non empty TopSpace
for f being Function of T,S
for P being Subset-Family of T holds union P c= union (f " (f .: P))

proof end;

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_a_cover_of P & B is finite ) holds
ex G being Subset-Family of S st
( G c= F & G is_a_cover_of f .: P & G is finite )

proof end;

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

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

end;

:: deftheorem defines [#] WEIERSTR:def 3 :

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

end;

:: deftheorem defines upper_bound WEIERSTR:def 4 :

:: deftheorem defines lower_bound WEIERSTR:def 5 :

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;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines dist WEIERSTR:def 6 :

theorem Th22: :: WEIERSTR:22

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

proof end;

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

proof end;

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

proof end;

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

proof end;

uniqueness

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines dist_max WEIERSTR:def 7 :

:: deftheorem Def8 defines dist_min WEIERSTR:def 8 :

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;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 ;
func max_dist_min P,Q -> Real equals :: WEIERSTR:def 10
upper_bound ((dist_min P) .: Q);
correctness ;
func min_dist_max P,Q -> Real equals :: WEIERSTR:def 11
lower_bound ((dist_max P) .: Q);
correctness ;
func max_dist_max P,Q -> Real equals :: WEIERSTR:def 12
upper_bound ((dist_max P) .: Q);
correctness ;

end;

:: deftheorem defines min_dist_min WEIERSTR:def 9 :

:: deftheorem defines max_dist_min WEIERSTR:def 10 :

:: deftheorem defines min_dist_max WEIERSTR:def 11 :

:: deftheorem defines max_dist_max WEIERSTR:def 12 :

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

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

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;