:: HAUSDORF semantic presentation

definition
let c1 be real number ;
redefine func { as {c1} -> Subset of REAL ;
coherence
{c1} is Subset of REAL
proof end;
end;

registration
let c1 be non empty MetrSpace;
cluster TopSpaceMetr a1 -> being_T2 ;
coherence
TopSpaceMetr c1 is being_T2
by PCOMPS_1:38;
end;

theorem Th1: :: HAUSDORF:1
for b1, b2 being real number st b1 >= 0 & b2 >= 0 & max b1,b2 = 0 holds
b1 = 0
proof end;

theorem Th2: :: HAUSDORF:2
for b1 being non empty MetrSpace
for b2 being Point of b1 holds (dist b2) . b2 = 0
proof end;

theorem Th3: :: HAUSDORF:3
for b1 being non empty MetrSpace
for b2 being Subset of (TopSpaceMetr b1)
for b3 being Point of b1 st b3 in b2 holds
0 in (dist b3) .: b2
proof end;

theorem Th4: :: HAUSDORF:4
for b1 being non empty MetrSpace
for b2 being Subset of (TopSpaceMetr b1)
for b3 being Point of b1
for b4 being real number st b4 in (dist b3) .: b2 holds
b4 >= 0
proof end;

theorem Th5: :: HAUSDORF:5
for b1 being non empty MetrSpace
for b2 being Subset of (TopSpaceMetr b1)
for b3 being set st b3 in b2 holds
(dist_min b2) . b3 = 0
proof end;

theorem Th6: :: HAUSDORF:6
for b1 being non empty MetrSpace
for b2 being Point of b1
for b3 being Point of (TopSpaceMetr b1)
for b4 being real number st b2 = b3 & b4 > 0 holds
Ball b2,b4 is a_neighborhood of b3
proof end;

theorem Th7: :: HAUSDORF:7
for b1 being non empty MetrSpace
for b2 being Subset of (TopSpaceMetr b1)
for b3 being Point of b1 holds
( b3 in Cl b2 iff for b4 being real number st b4 > 0 holds
Ball b3,b4 meets b2 )
proof end;

theorem Th8: :: HAUSDORF:8
for b1 being non empty MetrSpace
for b2 being Point of b1
for b3 being Subset of (TopSpaceMetr b1) holds
( b2 in Cl b3 iff for b4 being real number st b4 > 0 holds
ex b5 being Point of b1 st
( b5 in b3 & dist b2,b5 < b4 ) )
proof end;

theorem Th9: :: HAUSDORF:9
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3 being Point of b1 holds
( (dist_min b2) . b3 = 0 iff for b4 being real number st b4 > 0 holds
ex b5 being Point of b1 st
( b5 in b2 & dist b3,b5 < b4 ) )
proof end;

theorem Th10: :: HAUSDORF:10
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3 being Point of b1 holds
( b3 in Cl b2 iff (dist_min b2) . b3 = 0 )
proof end;

theorem Th11: :: HAUSDORF:11
for b1 being non empty MetrSpace
for b2 being non empty closed Subset of (TopSpaceMetr b1)
for b3 being Point of b1 holds
( b3 in b2 iff (dist_min b2) . b3 = 0 )
proof end;

theorem Th12: :: HAUSDORF:12
for b1 being non empty Subset of R^1 ex b2 being non empty Subset of REAL st
( b1 = b2 & lower_bound b1 = inf b2 )
proof end;

theorem Th13: :: HAUSDORF:13
for b1 being non empty Subset of R^1 ex b2 being non empty Subset of REAL st
( b1 = b2 & upper_bound b1 = sup b2 )
proof end;

theorem Th14: :: HAUSDORF:14
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3 being Point of b1
for b4 being Subset of REAL st b4 = (dist b3) .: b2 holds
b4 is bounded_below
proof end;

theorem Th15: :: HAUSDORF:15
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3, b4 being Point of b1 st b4 in b2 holds
(dist_min b2) . b3 <= dist b3,b4
proof end;

theorem Th16: :: HAUSDORF:16
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3 being real number
for b4 being Point of b1 st ( for b5 being Point of b1 st b5 in b2 holds
dist b4,b5 >= b3 ) holds
(dist_min b2) . b4 >= b3
proof end;

theorem Th17: :: HAUSDORF:17
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3, b4 being Point of b1 holds (dist_min b2) . b3 <= (dist b3,b4) + ((dist_min b2) . b4)
proof end;

theorem Th18: :: HAUSDORF:18
for b1 being non empty MetrSpace
for b2 being Subset of (TopSpaceMetr b1)
for b3 being non empty Subset of b1 st b2 = b3 holds
(TopSpaceMetr b1) | b2 = TopSpaceMetr (b1 | b3)
proof end;

theorem Th19: :: HAUSDORF:19
for b1 being non empty MetrSpace
for b2 being Subset of b1
for b3 being non empty Subset of b1
for b4 being Subset of (b1 | b3) st b2 c= b3 & b2 = b4 & b4 is bounded holds
b2 is bounded
proof end;

theorem Th20: :: HAUSDORF:20
for b1 being non empty MetrSpace
for b2 being Subset of b1
for b3 being Subset of (TopSpaceMetr b1) st b3 = b2 & b3 is compact holds
b2 is bounded
proof end;

theorem Th21: :: HAUSDORF:21
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3 being Point of b1 ex b4 being Point of b1 st
( b4 in b2 & (dist_min b2) . b3 <= dist b4,b3 )
proof end;

registration
let c1 be non empty MetrSpace;
let c2 be Point of c1;
cluster dist a2 -> continuous ;
coherence
dist c2 is continuous
by WEIERSTR:22;
end;

registration
let c1 be non empty MetrSpace;
let c2 be non empty compact Subset of (TopSpaceMetr c1);
cluster dist_max a2 -> continuous ;
coherence
dist_max c2 is continuous
by WEIERSTR:30;
cluster dist_min a2 -> continuous ;
coherence
dist_min c2 is continuous
by WEIERSTR:33;
end;

Lemma21: for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3 being Point of b1
for b4 being Subset of REAL st b4 = (dist b3) .: b2 & b2 is compact holds
b4 is bounded_above
proof end;

theorem Th22: :: HAUSDORF:22
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3, b4 being Point of b1 st b4 in b2 & b2 is compact holds
(dist_max b2) . b3 >= dist b3,b4
proof end;

theorem Th23: :: HAUSDORF:23
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3 being Point of b1 st b2 is compact holds
ex b4 being Point of b1 st
( b4 in b2 & (dist_max b2) . b3 >= dist b4,b3 )
proof end;

theorem Th24: :: HAUSDORF:24
for b1 being non empty MetrSpace
for b2, b3 being non empty Subset of (TopSpaceMetr b1)
for b4 being Point of b1 st b2 is compact & b3 is compact & b4 in b3 holds
(dist_min b2) . b4 <= max_dist_max b2,b3
proof end;

theorem Th25: :: HAUSDORF:25
for b1 being non empty MetrSpace
for b2, b3 being non empty Subset of (TopSpaceMetr b1)
for b4 being Point of b1 st b2 is compact & b3 is compact & b4 in b3 holds
(dist_max b2) . b4 <= max_dist_max b2,b3
proof end;

theorem Th26: :: HAUSDORF:26
for b1 being non empty MetrSpace
for b2, b3 being non empty Subset of (TopSpaceMetr b1)
for b4 being Subset of REAL st b4 = (dist_max b2) .: b3 & b2 is compact & b3 is compact holds
b4 is bounded_above
proof end;

theorem Th27: :: HAUSDORF:27
for b1 being non empty MetrSpace
for b2, b3 being non empty Subset of (TopSpaceMetr b1)
for b4 being Subset of REAL st b4 = (dist_min b2) .: b3 & b2 is compact & b3 is compact holds
b4 is bounded_above
proof end;

theorem Th28: :: HAUSDORF:28
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1)
for b3 being Point of b1 st b2 is compact holds
(dist_min b2) . b3 <= (dist_max b2) . b3
proof end;

theorem Th29: :: HAUSDORF:29
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1) holds (dist_min b2) .: b2 = {0}
proof end;

theorem Th30: :: HAUSDORF:30
for b1 being non empty MetrSpace
for b2, b3 being non empty Subset of (TopSpaceMetr b1) st b2 is compact & b3 is compact holds
max_dist_min b2,b3 >= 0
proof end;

theorem Th31: :: HAUSDORF:31
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1) holds max_dist_min b2,b2 = 0
proof end;

theorem Th32: :: HAUSDORF:32
for b1 being non empty MetrSpace
for b2, b3 being non empty Subset of (TopSpaceMetr b1) st b2 is compact & b3 is compact holds
min_dist_max b2,b3 >= 0
proof end;

theorem Th33: :: HAUSDORF:33
for b1 being non empty MetrSpace
for b2, b3 being non empty Subset of (TopSpaceMetr b1)
for b4 being Point of b1 st b2 is compact & b3 is compact & b4 in b2 holds
(dist_min b3) . b4 <= max_dist_min b3,b2
proof end;

definition
let c1 be non empty MetrSpace;
let c2, c3 be Subset of (TopSpaceMetr c1);
func HausDist c2,c3 -> Real equals :: HAUSDORF:def 1
max (max_dist_min a2,a3),(max_dist_min a3,a2);
coherence
max (max_dist_min c2,c3),(max_dist_min c3,c2) is Real
;
commutativity
for b1 being Real
for b2, b3 being Subset of (TopSpaceMetr c1) st b1 = max (max_dist_min b2,b3),(max_dist_min b3,b2) holds
b1 = max (max_dist_min b3,b2),(max_dist_min b2,b3)
;
end;

:: deftheorem Def1 defines HausDist HAUSDORF:def 1 :
for b1 being non empty MetrSpace
for b2, b3 being Subset of (TopSpaceMetr b1) holds HausDist b2,b3 = max (max_dist_min b2,b3),(max_dist_min b3,b2);

theorem Th34: :: HAUSDORF:34
for b1 being non empty MetrSpace
for b2, b3 being non empty Subset of (TopSpaceMetr b1)
for b4 being Point of b1 st b2 is compact & b3 is compact & b4 in b2 holds
(dist_min b3) . b4 <= HausDist b2,b3
proof end;

theorem Th35: :: HAUSDORF:35
for b1 being non empty MetrSpace
for b2, b3, b4 being non empty Subset of (TopSpaceMetr b1) st b2 is compact & b3 is compact & b4 is compact holds
max_dist_min b2,b4 <= (HausDist b2,b3) + (HausDist b3,b4)
proof end;

theorem Th36: :: HAUSDORF:36
for b1 being non empty MetrSpace
for b2, b3, b4 being non empty Subset of (TopSpaceMetr b1) st b2 is compact & b3 is compact & b4 is compact holds
max_dist_min b4,b2 <= (HausDist b2,b3) + (HausDist b3,b4)
proof end;

theorem Th37: :: HAUSDORF:37
for b1 being non empty MetrSpace
for b2, b3 being non empty Subset of (TopSpaceMetr b1) st b2 is compact & b3 is compact holds
HausDist b2,b3 >= 0
proof end;

theorem Th38: :: HAUSDORF:38
for b1 being non empty MetrSpace
for b2 being non empty Subset of (TopSpaceMetr b1) holds HausDist b2,b2 = 0 by Th31;

theorem Th39: :: HAUSDORF:39
for b1 being non empty MetrSpace
for b2, b3 being non empty Subset of (TopSpaceMetr b1) st b2 is compact & b3 is compact & HausDist b2,b3 = 0 holds
b2 = b3
proof end;

theorem Th40: :: HAUSDORF:40
for b1 being non empty MetrSpace
for b2, b3, b4 being non empty Subset of (TopSpaceMetr b1) st b2 is compact & b3 is compact & b4 is compact holds
HausDist b2,b4 <= (HausDist b2,b3) + (HausDist b3,b4)
proof end;

definition
let c1 be Nat;
let c2, c3 be Subset of (TOP-REAL c1);
func max_dist_min c2,c3 -> Real means :: HAUSDORF:def 2
ex b1, b2 being Subset of (TopSpaceMetr (Euclid a1)) st
( a2 = b1 & a3 = b2 & a4 = max_dist_min b1,b2 );
existence
ex b1 being Realex b2, b3 being Subset of (TopSpaceMetr (Euclid c1)) st
( c2 = b2 & c3 = b3 & b1 = max_dist_min b2,b3 )
proof end;
uniqueness
for b1, b2 being Real st ex b3, b4 being Subset of (TopSpaceMetr (Euclid c1)) st
( c2 = b3 & c3 = b4 & b1 = max_dist_min b3,b4 ) & ex b3, b4 being Subset of (TopSpaceMetr (Euclid c1)) st
( c2 = b3 & c3 = b4 & b2 = max_dist_min b3,b4 ) holds
b1 = b2
;
end;

:: deftheorem Def2 defines max_dist_min HAUSDORF:def 2 :
for b1 being Nat
for b2, b3 being Subset of (TOP-REAL b1)
for b4 being Real holds
( b4 = max_dist_min b2,b3 iff ex b5, b6 being Subset of (TopSpaceMetr (Euclid b1)) st
( b2 = b5 & b3 = b6 & b4 = max_dist_min b5,b6 ) );

definition
let c1 be Nat;
let c2, c3 be Subset of (TOP-REAL c1);
func HausDist c2,c3 -> Real means :Def3: :: HAUSDORF:def 3
ex b1, b2 being Subset of (TopSpaceMetr (Euclid a1)) st
( a2 = b1 & a3 = b2 & a4 = HausDist b1,b2 );
existence
ex b1 being Realex b2, b3 being Subset of (TopSpaceMetr (Euclid c1)) st
( c2 = b2 & c3 = b3 & b1 = HausDist b2,b3 )
proof end;
uniqueness
for b1, b2 being Real st ex b3, b4 being Subset of (TopSpaceMetr (Euclid c1)) st
( c2 = b3 & c3 = b4 & b1 = HausDist b3,b4 ) & ex b3, b4 being Subset of (TopSpaceMetr (Euclid c1)) st
( c2 = b3 & c3 = b4 & b2 = HausDist b3,b4 ) holds
b1 = b2
;
commutativity
for b1 being Real
for b2, b3 being Subset of (TOP-REAL c1) st ex b4, b5 being Subset of (TopSpaceMetr (Euclid c1)) st
( b2 = b4 & b3 = b5 & b1 = HausDist b4,b5 ) holds
ex b4, b5 being Subset of (TopSpaceMetr (Euclid c1)) st
( b3 = b4 & b2 = b5 & b1 = HausDist b4,b5 )
;
end;

:: deftheorem Def3 defines HausDist HAUSDORF:def 3 :
for b1 being Nat
for b2, b3 being Subset of (TOP-REAL b1)
for b4 being Real holds
( b4 = HausDist b2,b3 iff ex b5, b6 being Subset of (TopSpaceMetr (Euclid b1)) st
( b2 = b5 & b3 = b6 & b4 = HausDist b5,b6 ) );

theorem Th41: :: HAUSDORF:41
for b1 being Nat
for b2, b3 being non empty Subset of (TOP-REAL b1) st b2 is compact & b3 is compact holds
HausDist b2,b3 >= 0
proof end;

theorem Th42: :: HAUSDORF:42
for b1 being Nat
for b2 being non empty Subset of (TOP-REAL b1) holds HausDist b2,b2 = 0
proof end;

theorem Th43: :: HAUSDORF:43
for b1 being Nat
for b2, b3 being non empty Subset of (TOP-REAL b1) st b2 is compact & b3 is compact & HausDist b2,b3 = 0 holds
b2 = b3
proof end;

theorem Th44: :: HAUSDORF:44
for b1 being Nat
for b2, b3, b4 being non empty Subset of (TOP-REAL b1) st b2 is compact & b3 is compact & b4 is compact holds
HausDist b2,b4 <= (HausDist b2,b3) + (HausDist b3,b4)
proof end;