:: HAUSDORF semantic presentation

definition

let c₁ be real number ;
redefine func { as {c₁} -> Subset of REAL ;
coherence

proof end;

end;

registration

let c₁ be non empty MetrSpace;
cluster TopSpaceMetr a₁ -> being_T2 ;
coherence by PCOMPS_1:38;

end;

theorem Th1: :: HAUSDORF:1

for b₁, b₂ being real number st b₁ >= 0 & b₂ >= 0 & max b₁,b₂ = 0 holds
b₁ = 0

proof end;

theorem Th2: :: HAUSDORF:2

for b₁ being non empty MetrSpace
for b₂ being Point of b₁ holds (dist b₂) . b₂ = 0

proof end;

theorem Th3: :: HAUSDORF:3

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁)
for b₃ being Point of b₁ st b₃ in b₂ holds
0 in (dist b₃) .: b₂

proof end;

theorem Th4: :: HAUSDORF:4

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁)
for b₃ being Point of b₁
for b₄ being real number st b₄ in (dist b₃) .: b₂ holds
b₄ >= 0

proof end;

theorem Th5: :: HAUSDORF:5

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁)
for b₃ being set st b₃ in b₂ holds
(dist_min b₂) . b₃ = 0

proof end;

theorem Th6: :: HAUSDORF:6

for b₁ being non empty MetrSpace
for b₂ being Point of b₁
for b₃ being Point of (TopSpaceMetr b₁)
for b₄ being real number st b₂ = b₃ & b₄ > 0 holds
Ball b₂,b₄ is a_neighborhood of b₃

proof end;

theorem Th7: :: HAUSDORF:7

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁)
for b₃ being Point of b₁ holds
( b₃ in Cl b₂ iff for b₄ being real number st b₄ > 0 holds
Ball b₃,b₄ meets b₂ )

proof end;

theorem Th8: :: HAUSDORF:8

for b₁ being non empty MetrSpace
for b₂ being Point of b₁
for b₃ being Subset of (TopSpaceMetr b₁) holds
( b₂ in Cl b₃ iff for b₄ being real number st b₄ > 0 holds
ex b₅ being Point of b₁ st
( b₅ in b₃ & dist b₂,b₅ < b₄ ) )

proof end;

theorem Th9: :: HAUSDORF:9

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃ being Point of b₁ holds
( (dist_min b₂) . b₃ = 0 iff for b₄ being real number st b₄ > 0 holds
ex b₅ being Point of b₁ st
( b₅ in b₂ & dist b₃,b₅ < b₄ ) )

proof end;

theorem Th10: :: HAUSDORF:10

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃ being Point of b₁ holds
( b₃ in Cl b₂ iff (dist_min b₂) . b₃ = 0 )

proof end;

theorem Th11: :: HAUSDORF:11

for b₁ being non empty MetrSpace
for b₂ being non empty closed Subset of (TopSpaceMetr b₁)
for b₃ being Point of b₁ holds
( b₃ in b₂ iff (dist_min b₂) . b₃ = 0 )

proof end;

theorem Th12: :: HAUSDORF:12

for b₁ being non empty Subset of R^1 ex b₂ being non empty Subset of REAL st
( b₁ = b₂ & lower_bound b₁ = inf b₂ )

proof end;

theorem Th13: :: HAUSDORF:13

for b₁ being non empty Subset of R^1 ex b₂ being non empty Subset of REAL st
( b₁ = b₂ & upper_bound b₁ = sup b₂ )

proof end;

theorem Th14: :: HAUSDORF:14

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃ being Point of b₁
for b₄ being Subset of REAL st b₄ = (dist b₃) .: b₂ holds
b₄ is bounded_below

proof end;

theorem Th15: :: HAUSDORF:15

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃, b₄ being Point of b₁ st b₄ in b₂ holds
(dist_min b₂) . b₃ <= dist b₃,b₄

proof end;

theorem Th16: :: HAUSDORF:16

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃ being real number
for b₄ being Point of b₁ st ( for b₅ being Point of b₁ st b₅ in b₂ holds
dist b₄,b₅ >= b₃ ) holds
(dist_min b₂) . b₄ >= b₃

proof end;

theorem Th17: :: HAUSDORF:17

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃, b₄ being Point of b₁ holds (dist_min b₂) . b₃ <= (dist b₃,b₄) + ((dist_min b₂) . b₄)

proof end;

theorem Th18: :: HAUSDORF:18

for b₁ being non empty MetrSpace
for b₂ being Subset of (TopSpaceMetr b₁)
for b₃ being non empty Subset of b₁ st b₂ = b₃ holds
(TopSpaceMetr b₁) | b₂ = TopSpaceMetr (b₁ | b₃)

proof end;

theorem Th19: :: HAUSDORF:19

for b₁ being non empty MetrSpace
for b₂ being Subset of b₁
for b₃ being non empty Subset of b₁
for b₄ being Subset of (b₁ | b₃) st b₂ c= b₃ & b₂ = b₄ & b₄ is bounded holds
b₂ is bounded

proof end;

theorem Th20: :: HAUSDORF:20

for b₁ being non empty MetrSpace
for b₂ being Subset of b₁
for b₃ being Subset of (TopSpaceMetr b₁) st b₃ = b₂ & b₃ is compact holds
b₂ is bounded

proof end;

theorem Th21: :: HAUSDORF:21

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃ being Point of b₁ ex b₄ being Point of b₁ st
( b₄ in b₂ & (dist_min b₂) . b₃ <= dist b₄,b₃ )

proof end;

registration

let c₁ be non empty MetrSpace;
let c₂ be Point of c₁;
cluster dist a₂ -> continuous ;
coherence by WEIERSTR:22;

end;

registration

let c₁ be non empty MetrSpace;
let c₂ be non empty compact Subset of (TopSpaceMetr c₁);
cluster dist_max a₂ -> continuous ;
coherence by WEIERSTR:30;
cluster dist_min a₂ -> continuous ;
coherence by WEIERSTR:33;

end;

Lemma21: for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃ being Point of b₁
for b₄ being Subset of REAL st b₄ = (dist b₃) .: b₂ & b₂ is compact holds
b₄ is bounded_above

proof end;

theorem Th22: :: HAUSDORF:22

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃, b₄ being Point of b₁ st b₄ in b₂ & b₂ is compact holds
(dist_max b₂) . b₃ >= dist b₃,b₄

proof end;

theorem Th23: :: HAUSDORF:23

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

proof end;

theorem Th24: :: HAUSDORF:24

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

proof end;

theorem Th25: :: HAUSDORF:25

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

proof end;

theorem Th26: :: HAUSDORF:26

for b₁ being non empty MetrSpace
for b₂, b₃ being non empty Subset of (TopSpaceMetr b₁)
for b₄ being Subset of REAL st b₄ = (dist_max b₂) .: b₃ & b₂ is compact & b₃ is compact holds
b₄ is bounded_above

proof end;

theorem Th27: :: HAUSDORF:27

for b₁ being non empty MetrSpace
for b₂, b₃ being non empty Subset of (TopSpaceMetr b₁)
for b₄ being Subset of REAL st b₄ = (dist_min b₂) .: b₃ & b₂ is compact & b₃ is compact holds
b₄ is bounded_above

proof end;

theorem Th28: :: HAUSDORF:28

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁)
for b₃ being Point of b₁ st b₂ is compact holds
(dist_min b₂) . b₃ <= (dist_max b₂) . b₃

proof end;

theorem Th29: :: HAUSDORF:29

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁) holds (dist_min b₂) .: b₂ = {0}

proof end;

theorem Th30: :: HAUSDORF:30

for b₁ being non empty MetrSpace
for b₂, b₃ being non empty Subset of (TopSpaceMetr b₁) st b₂ is compact & b₃ is compact holds
max_dist_min b₂,b₃ >= 0

proof end;

theorem Th31: :: HAUSDORF:31

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁) holds max_dist_min b₂,b₂ = 0

proof end;

theorem Th32: :: HAUSDORF:32

for b₁ being non empty MetrSpace
for b₂, b₃ being non empty Subset of (TopSpaceMetr b₁) st b₂ is compact & b₃ is compact holds
min_dist_max b₂,b₃ >= 0

proof end;

theorem Th33: :: HAUSDORF:33

for b₁ being non empty MetrSpace
for b₂, b₃ being non empty Subset of (TopSpaceMetr b₁)
for b₄ being Point of b₁ st b₂ is compact & b₃ is compact & b₄ in b₂ holds
(dist_min b₃) . b₄ <= max_dist_min b₃,b₂

proof end;

definition

let c₁ be non empty MetrSpace;
let c₂, c₃ be Subset of (TopSpaceMetr c₁);
func HausDist c₂,c₃ -> Real equals :: HAUSDORF:def 1
max (max_dist_min a₂,a₃),(max_dist_min a₃,a₂);
coherence ;
commutativity ;

end;

:: deftheorem Def1 defines HausDist HAUSDORF:def 1 :

theorem Th34: :: HAUSDORF:34

for b₁ being non empty MetrSpace
for b₂, b₃ being non empty Subset of (TopSpaceMetr b₁)
for b₄ being Point of b₁ st b₂ is compact & b₃ is compact & b₄ in b₂ holds
(dist_min b₃) . b₄ <= HausDist b₂,b₃

proof end;

theorem Th35: :: HAUSDORF:35

for b₁ being non empty MetrSpace
for b₂, b₃, b₄ being non empty Subset of (TopSpaceMetr b₁) st b₂ is compact & b₃ is compact & b₄ is compact holds
max_dist_min b₂,b₄ <= (HausDist b₂,b₃) + (HausDist b₃,b₄)

proof end;

theorem Th36: :: HAUSDORF:36

for b₁ being non empty MetrSpace
for b₂, b₃, b₄ being non empty Subset of (TopSpaceMetr b₁) st b₂ is compact & b₃ is compact & b₄ is compact holds
max_dist_min b₄,b₂ <= (HausDist b₂,b₃) + (HausDist b₃,b₄)

proof end;

theorem Th37: :: HAUSDORF:37

for b₁ being non empty MetrSpace
for b₂, b₃ being non empty Subset of (TopSpaceMetr b₁) st b₂ is compact & b₃ is compact holds
HausDist b₂,b₃ >= 0

proof end;

theorem Th38: :: HAUSDORF:38

for b₁ being non empty MetrSpace
for b₂ being non empty Subset of (TopSpaceMetr b₁) holds HausDist b₂,b₂ = 0 by Th31;

theorem Th39: :: HAUSDORF:39

for b₁ being non empty MetrSpace
for b₂, b₃ being non empty Subset of (TopSpaceMetr b₁) st b₂ is compact & b₃ is compact & HausDist b₂,b₃ = 0 holds
b₂ = b₃

proof end;

theorem Th40: :: HAUSDORF:40

for b₁ being non empty MetrSpace
for b₂, b₃, b₄ being non empty Subset of (TopSpaceMetr b₁) st b₂ is compact & b₃ is compact & b₄ is compact holds
HausDist b₂,b₄ <= (HausDist b₂,b₃) + (HausDist b₃,b₄)

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Subset of (TOP-REAL c₁);
func max_dist_min c₂,c₃ -> Real means :: HAUSDORF:def 2
ex b₁, b₂ being Subset of (TopSpaceMetr (Euclid a₁)) st
( a₂ = b₁ & a₃ = b₂ & a₄ = max_dist_min b₁,b₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines max_dist_min HAUSDORF:def 2 :

definition

let c₁ be Nat;
let c₂, c₃ be Subset of (TOP-REAL c₁);
func HausDist c₂,c₃ -> Real means :Def3: :: HAUSDORF:def 3
ex b₁, b₂ being Subset of (TopSpaceMetr (Euclid a₁)) st
( a₂ = b₁ & a₃ = b₂ & a₄ = HausDist b₁,b₂ );
existence

proof end;

uniqueness ;
commutativity ;

end;

:: deftheorem Def3 defines HausDist HAUSDORF:def 3 :

theorem Th41: :: HAUSDORF:41

for b₁ being Nat
for b₂, b₃ being non empty Subset of (TOP-REAL b₁) st b₂ is compact & b₃ is compact holds
HausDist b₂,b₃ >= 0

proof end;

theorem Th42: :: HAUSDORF:42

for b₁ being Nat
for b₂ being non empty Subset of (TOP-REAL b₁) holds HausDist b₂,b₂ = 0

proof end;

theorem Th43: :: HAUSDORF:43

for b₁ being Nat
for b₂, b₃ being non empty Subset of (TOP-REAL b₁) st b₂ is compact & b₃ is compact & HausDist b₂,b₃ = 0 holds
b₂ = b₃

proof end;

theorem Th44: :: HAUSDORF:44

for b₁ being Nat
for b₂, b₃, b₄ being non empty Subset of (TOP-REAL b₁) st b₂ is compact & b₃ is compact & b₄ is compact holds
HausDist b₂,b₄ <= (HausDist b₂,b₃) + (HausDist b₃,b₄)

proof end;