:: WEIERSTR semantic presentation

theorem Th1: :: WEIERSTR:1

for b₁ being MetrSpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being Real ex b₆ being Point of b₁ex b₇ being Real st (Ball b₂,b₄) \/ (Ball b₃,b₅) c= Ball b₆,b₇

proof end;

theorem Th2: :: WEIERSTR:2

for b₁ being MetrSpace
for b₂ being Nat
for b₃ being Subset-Family of b₁
for b₄ being FinSequence st b₃ is finite & b₃ is_ball-family & rng b₄ = b₃ & dom b₄ = Seg (b₂ + 1) holds
ex b₅ being Subset-Family of b₁ st
( b₅ is finite & b₅ is_ball-family & ex b₆ being FinSequence st
( rng b₆ = b₅ & dom b₆ = Seg b₂ & ex b₇ being Point of b₁ex b₈ being Real st union b₃ c= (union b₅) \/ (Ball b₇,b₈) ) )

proof end;

theorem Th3: :: WEIERSTR:3

for b₁ being MetrSpace
for b₂ being Subset-Family of b₁ st b₂ is finite & b₂ is_ball-family holds
ex b₃ being Point of b₁ex b₄ being Real st union b₂ c= Ball b₃,b₄

proof end;

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be Function of c₁,c₂;
let c₄ be Subset-Family of c₂;
func c₃ " c₄ -> Subset-Family of a₁ means :Def1: :: WEIERSTR:def 1
for b₁ being Subset of a₁ holds
( b₁ in a₅ iff ex b₂ being Subset of a₂ st
( b₂ in a₄ & b₁ = a₃ " b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines " WEIERSTR:def 1 :

theorem Th4: :: WEIERSTR:4

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄, b₅ being Subset-Family of b₂ st b₄ c= b₅ holds
b₃ " b₄ c= b₃ " b₅

proof end;

theorem Th5: :: WEIERSTR:5

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₂ st b₃ is continuous & b₄ is open holds
b₃ " b₄ is open

proof end;

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be Function of c₁,c₂;
let c₄ be Subset-Family of c₁;
func c₃ .: c₄ -> Subset-Family of a₂ means :Def2: :: WEIERSTR:def 2
for b₁ being Subset of a₂ holds
( b₁ in a₅ iff ex b₂ being Subset of a₁ st
( b₂ in a₄ & b₁ = a₃ .: b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th6: :: WEIERSTR:6

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄, b₅ being Subset-Family of b₁ st b₄ c= b₅ holds
b₃ .: b₄ c= b₃ .: b₅

proof end;

theorem Th7: :: WEIERSTR:7

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₂
for b₅ being Subset of b₂ st b₃ .: (b₃ " b₄) is_a_cover_of b₅ holds
b₄ is_a_cover_of b₅

proof end;

theorem Th8: :: WEIERSTR:8

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₁
for b₅ being Subset of b₁ st b₄ is_a_cover_of b₅ holds
b₃ " (b₃ .: b₄) is_a_cover_of b₅

proof end;

theorem Th9: :: WEIERSTR:9

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₂ holds union (b₃ .: (b₃ " b₄)) c= union b₄

proof end;

theorem Th10: :: WEIERSTR:10

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₁ holds union b₄ c= union (b₃ " (b₃ .: b₄))

proof end;

theorem Th11: :: WEIERSTR:11

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₂ st b₄ is finite holds
b₃ " b₄ is finite

proof end;

theorem Th12: :: WEIERSTR:12

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₁ st b₄ is finite holds
b₃ .: b₄ is finite

proof end;

theorem Th13: :: WEIERSTR:13

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁
for b₅ being Subset-Family of b₂ st ex b₆ being Subset-Family of b₁ st
( b₆ c= b₃ " b₅ & b₆ is_a_cover_of b₄ & b₆ is finite ) holds
ex b₆ being Subset-Family of b₂ st
( b₆ c= b₅ & b₆ is_a_cover_of b₃ .: b₄ & b₆ is finite )

proof end;

theorem Th14: :: WEIERSTR:14

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁ st b₄ is compact & b₃ is continuous holds
b₃ .: b₄ is compact

proof end;

theorem Th15: :: WEIERSTR:15

for b₁ being non empty TopSpace
for b₂ being Function of b₁,R^1
for b₃ being Subset of b₁ st b₃ is compact & b₂ is continuous holds
b₂ .: b₃ is compact by Th14;

theorem Th16: :: WEIERSTR:16

for b₁ being Function of (TOP-REAL 2),R^1
for b₂ being Subset of (TOP-REAL 2) st b₂ is compact & b₁ is continuous holds
b₁ .: b₂ is compact by Th14;

definition

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

end;

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

theorem Th17: :: WEIERSTR:17

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

proof end;

theorem Th18: :: WEIERSTR:18

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

proof end;

theorem Th19: :: WEIERSTR:19

for b₁ being Subset of R^1 st b₁ is compact holds
[#] b₁ is compact

proof end;

Lemma12: for b₁ being non empty TopSpace
for b₂ being Function of b₁,R^1
for b₃ being Subset of b₁ st b₃ <> {} & b₃ is compact & b₂ is continuous holds
ex b₄, b₅ being Point of b₁ st
( b₄ in b₃ & b₅ in b₃ & b₂ . b₄ = upper_bound ([#] (b₂ .: b₃)) & b₂ . b₅ = lower_bound ([#] (b₂ .: b₃)) )

proof end;

definition

let c₁ be Subset of R^1 ;
func upper_bound c₁ -> Real equals :: WEIERSTR:def 4
upper_bound ([#] a₁);
correctness ;
func lower_bound c₁ -> Real equals :: WEIERSTR:def 5
lower_bound ([#] a₁);
correctness ;

end;

:: deftheorem Def4 defines upper_bound WEIERSTR:def 4 :

:: deftheorem Def5 defines lower_bound WEIERSTR:def 5 :

theorem Th20: :: WEIERSTR:20

for b₁ being non empty TopSpace
for b₂ being Function of b₁,R^1
for b₃ being Subset of b₁ st b₃ <> {} & b₃ is compact & b₂ is continuous holds
ex b₄ being Point of b₁ st
( b₄ in b₃ & b₂ . b₄ = upper_bound (b₂ .: b₃) )

proof end;

theorem Th21: :: WEIERSTR:21

for b₁ being non empty TopSpace
for b₂ being Function of b₁,R^1
for b₃ being Subset of b₁ st b₃ <> {} & b₃ is compact & b₂ is continuous holds
ex b₄ being Point of b₁ st
( b₄ in b₃ & b₂ . b₄ = lower_bound (b₂ .: b₃) )

proof end;

definition

let c₁ be non empty MetrSpace;
let c₂ be Point of c₁;
func dist c₂ -> Function of (TopSpaceMetr a₁),R^1 means :Def6: :: WEIERSTR:def 6
for b₁ being Point of a₁ holds a₃ . b₁ = dist b₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines dist WEIERSTR:def 6 :

theorem Th22: :: WEIERSTR:22

for b₁ being non empty MetrSpace
for b₂ being Point of b₁ holds dist b₂ is continuous

proof end;

theorem Th23: :: WEIERSTR:23

for b₁ being non empty MetrSpace
for b₂ being Point of b₁
for b₃ being Subset of (TopSpaceMetr b₁) st b₃ <> {} & b₃ is compact holds
ex b₄ being Point of (TopSpaceMetr b₁) st
( b₄ in b₃ & (dist b₂) . b₄ = upper_bound ((dist b₂) .: b₃) )

proof end;

theorem Th24: :: WEIERSTR:24

proof end;

definition

let c₁ be non empty MetrSpace;
let c₂ be Subset of (TopSpaceMetr c₁);
func dist_max c₂ -> Function of (TopSpaceMetr a₁),R^1 means :Def7: :: WEIERSTR:def 7
for b₁ being Point of a₁ holds a₃ . b₁ = upper_bound ((dist b₁) .: a₂);
existence

proof end;

uniqueness

proof end;

func dist_min c₂ -> Function of (TopSpaceMetr a₁),R^1 means :Def8: :: WEIERSTR:def 8
for b₁ being Point of a₁ holds a₃ . b₁ = lower_bound ((dist b₁) .: a₂);
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 b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁) st b₂ is compact holds
for b₃, b₄ being Point of b₁ st b₃ in b₂ holds
( dist b₃,b₄ <= upper_bound ((dist b₄) .: b₂) & lower_bound ((dist b₄) .: b₂) <= dist b₃,b₄ )

proof end;

theorem Th26: :: WEIERSTR:26

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact holds
for b₃, b₄ being Point of b₁ holds abs ((upper_bound ((dist b₃) .: b₂)) - (upper_bound ((dist b₄) .: b₂))) <= dist b₃,b₄

proof end;

theorem Th27: :: WEIERSTR:27

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact holds
for b₃, b₄ being Point of b₁
for b₅, b₆ being Real st b₅ = (dist_max b₂) . b₃ & b₆ = (dist_max b₂) . b₄ holds
abs (b₅ - b₆) <= dist b₃,b₄

proof end;

theorem Th28: :: WEIERSTR:28

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact holds
for b₃, b₄ being Point of b₁ holds abs ((lower_bound ((dist b₃) .: b₂)) - (lower_bound ((dist b₄) .: b₂))) <= dist b₃,b₄

proof end;

theorem Th29: :: WEIERSTR:29

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact holds
for b₃, b₄ being Point of b₁
for b₅, b₆ being Real st b₅ = (dist_min b₂) . b₃ & b₆ = (dist_min b₂) . b₄ holds
abs (b₅ - b₆) <= dist b₃,b₄

proof end;

theorem Th30: :: WEIERSTR:30

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact holds
dist_max b₂ is continuous

proof end;

theorem Th31: :: WEIERSTR:31

for b₁ being non empty MetrSpace
for b₂, b₃ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact & b₃ <> {} & b₃ is compact holds
ex b₄ being Point of (TopSpaceMetr b₁) st
( b₄ in b₃ & (dist_max b₂) . b₄ = upper_bound ((dist_max b₂) .: b₃) )

proof end;

theorem Th32: :: WEIERSTR:32

proof end;

theorem Th33: :: WEIERSTR:33

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact holds
dist_min b₂ is continuous

proof end;

theorem Th34: :: WEIERSTR:34

for b₁ being non empty MetrSpace
for b₂, b₃ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact & b₃ <> {} & b₃ is compact holds
ex b₄ being Point of (TopSpaceMetr b₁) st
( b₄ in b₃ & (dist_min b₂) . b₄ = upper_bound ((dist_min b₂) .: b₃) )

proof end;

theorem Th35: :: WEIERSTR:35

for b₁ being non empty MetrSpace
for b₂, b₃ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact & b₃ <> {} & b₃ is compact holds
ex b₄ being Point of (TopSpaceMetr b₁) st
( b₄ in b₃ & (dist_min b₂) . b₄ = lower_bound ((dist_min b₂) .: b₃) )

proof end;

definition

let c₁ be non empty MetrSpace;
let c₂, c₃ be Subset of (TopSpaceMetr c₁);
func min_dist_min c₂,c₃ -> Real equals :: WEIERSTR:def 9
lower_bound ((dist_min a₂) .: a₃);
correctness ;
func max_dist_min c₂,c₃ -> Real equals :: WEIERSTR:def 10
upper_bound ((dist_min a₂) .: a₃);
correctness ;
func min_dist_max c₂,c₃ -> Real equals :: WEIERSTR:def 11
lower_bound ((dist_max a₂) .: a₃);
correctness ;
func max_dist_max c₂,c₃ -> Real equals :: WEIERSTR:def 12
upper_bound ((dist_max a₂) .: a₃);
correctness ;

end;

:: deftheorem Def9 defines min_dist_min WEIERSTR:def 9 :

:: deftheorem Def10 defines max_dist_min WEIERSTR:def 10 :

:: deftheorem Def11 defines min_dist_max WEIERSTR:def 11 :

:: deftheorem Def12 defines max_dist_max WEIERSTR:def 12 :

theorem Th36: :: WEIERSTR:36

for b₁ being non empty MetrSpace
for b₂, b₃ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact & b₃ <> {} & b₃ is compact holds
ex b₄, b₅ being Point of b₁ st
( b₄ in b₂ & b₅ in b₃ & dist b₄,b₅ = min_dist_min b₂,b₃ )

proof end;

theorem Th37: :: WEIERSTR:37

proof end;

theorem Th38: :: WEIERSTR:38

proof end;

theorem Th39: :: WEIERSTR:39

proof end;

theorem Th40: :: WEIERSTR:40

for b₁ being non empty MetrSpace
for b₂, b₃ being Subset of (TopSpaceMetr b₁) st b₂ is compact & b₃ is compact holds
for b₄, b₅ being Point of b₁ st b₄ in b₂ & b₅ in b₃ holds
( min_dist_min b₂,b₃ <= dist b₄,b₅ & dist b₄,b₅ <= max_dist_max b₂,b₃ )

proof end;