:: On the {H}ausdorff Distance Between Compact Subsets
:: by Adam Grabowski
::
:: Received January 27, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem Th1: :: HAUSDORF:1
theorem Th2: :: HAUSDORF:2
theorem Th3: :: HAUSDORF:3
theorem Th4: :: HAUSDORF:4
theorem Th5: :: HAUSDORF:5
theorem :: HAUSDORF:6
canceled;
theorem :: HAUSDORF:7
canceled;
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 :: HAUSDORF:20
theorem Th21: :: HAUSDORF:21
Lm1:
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for x being Point of M
for X being Subset of REAL st X = (dist x) .: P & P is compact holds
X is bounded_above
theorem Th22: :: HAUSDORF:22
theorem :: HAUSDORF:23
theorem Th24: :: HAUSDORF:24
theorem Th25: :: HAUSDORF:25
theorem :: HAUSDORF:26
theorem Th27: :: HAUSDORF:27
theorem :: HAUSDORF:28
theorem Th29: :: HAUSDORF:29
theorem Th30: :: HAUSDORF:30
theorem Th31: :: HAUSDORF:31
theorem :: HAUSDORF:32
theorem Th33: :: HAUSDORF:33
definition
let M be non
empty MetrSpace;
let P,
Q be
Subset of
(TopSpaceMetr M);
func HausDist P,
Q -> Real equals :: HAUSDORF:def 1
max (max_dist_min P,Q),
(max_dist_min Q,P);
coherence
max (max_dist_min P,Q),(max_dist_min Q,P) is Real
;
commutativity
for b1 being Real
for P, Q being Subset of (TopSpaceMetr M) st b1 = max (max_dist_min P,Q),(max_dist_min Q,P) holds
b1 = max (max_dist_min Q,P),(max_dist_min P,Q)
;
end;
:: deftheorem defines HausDist HAUSDORF:def 1 :
theorem Th34: :: HAUSDORF:34
theorem Th35: :: HAUSDORF:35
theorem Th36: :: HAUSDORF:36
theorem Th37: :: HAUSDORF:37
theorem :: HAUSDORF:38
theorem Th39: :: HAUSDORF:39
theorem Th40: :: HAUSDORF:40
definition
let n be
Element of
NAT ;
let P,
Q be
Subset of
(TOP-REAL n);
func max_dist_min P,
Q -> Real means :: HAUSDORF:def 2
ex
P',
Q' being
Subset of
(TopSpaceMetr (Euclid n)) st
(
P = P' &
Q = Q' &
it = max_dist_min P',
Q' );
existence
ex b1 being Real ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b1 = max_dist_min P',Q' )
uniqueness
for b1, b2 being Real st ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b1 = max_dist_min P',Q' ) & ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b2 = max_dist_min P',Q' ) holds
b1 = b2
;
end;
:: deftheorem defines max_dist_min HAUSDORF:def 2 :
definition
let n be
Element of
NAT ;
let P,
Q be
Subset of
(TOP-REAL n);
func HausDist P,
Q -> Real means :
Def3:
:: HAUSDORF:def 3
ex
P',
Q' being
Subset of
(TopSpaceMetr (Euclid n)) st
(
P = P' &
Q = Q' &
it = HausDist P',
Q' );
existence
ex b1 being Real ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b1 = HausDist P',Q' )
uniqueness
for b1, b2 being Real st ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b1 = HausDist P',Q' ) & ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b2 = HausDist P',Q' ) holds
b1 = b2
;
commutativity
for b1 being Real
for P, Q being Subset of (TOP-REAL n) st ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & b1 = HausDist P',Q' ) holds
ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( Q = P' & P = Q' & b1 = HausDist P',Q' )
;
end;
:: deftheorem Def3 defines HausDist HAUSDORF:def 3 :
theorem :: HAUSDORF:41
theorem :: HAUSDORF:42
theorem :: HAUSDORF:43
theorem :: HAUSDORF:44