:: HAUSDORF semantic presentation
theorem Th1: :: HAUSDORF:1
theorem Th2: :: HAUSDORF:2
theorem Th3: :: HAUSDORF:3
theorem Th4: :: HAUSDORF:4
theorem Th5: :: HAUSDORF:5
theorem Th6: :: HAUSDORF:6
theorem Th7: :: HAUSDORF:7
theorem Th8: :: HAUSDORF:8
theorem Th9: :: HAUSDORF:9
theorem Th10: :: HAUSDORF:10
theorem Th11: :: HAUSDORF:11
theorem Th12: :: HAUSDORF:12
theorem Th13: :: HAUSDORF:13
theorem Th14: :: HAUSDORF:14
theorem Th15: :: HAUSDORF:15
theorem Th16: :: HAUSDORF:16
theorem Th17: :: HAUSDORF:17
theorem Th18: :: HAUSDORF:18
theorem Th19: :: HAUSDORF:19
theorem Th20: :: HAUSDORF:20
theorem Th21: :: HAUSDORF:21
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
theorem Th22: :: HAUSDORF:22
theorem Th23: :: HAUSDORF:23
theorem Th24: :: HAUSDORF:24
theorem Th25: :: HAUSDORF:25
theorem Th26: :: HAUSDORF:26
theorem Th27: :: HAUSDORF:27
theorem Th28: :: HAUSDORF:28
theorem Th29: :: HAUSDORF:29
theorem Th30: :: HAUSDORF:30
theorem Th31: :: HAUSDORF:31
theorem Th32: :: HAUSDORF:32
theorem Th33: :: HAUSDORF:33
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 :
theorem Th34: :: HAUSDORF:34
theorem Th35: :: HAUSDORF:35
theorem Th36: :: HAUSDORF:36
theorem Th37: :: HAUSDORF:37
theorem Th38: :: HAUSDORF:38
theorem Th39: :: HAUSDORF:39
theorem Th40: :: HAUSDORF:40
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 )
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 :
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 )
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 :
theorem Th41: :: HAUSDORF:41
theorem Th42: :: HAUSDORF:42
theorem Th43: :: HAUSDORF:43
theorem Th44: :: HAUSDORF:44