:: On the {H}ausdorff Distance Between Compact Subsets :: by Adam Grabowski :: :: Received January 27, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin registration let M be non empty MetrSpace; cluster TopSpaceMetr M -> T_2 ; coherence TopSpaceMetr M is T_2 by PCOMPS_1:34; end; theorem Th1: :: HAUSDORF:1 for x, y being real number st x >= 0 & max (x,y) = 0 holds x = 0 proofend; theorem Th2: :: HAUSDORF:2 for M being non empty MetrSpace for x being Point of M holds (dist x) . x = 0 proofend; theorem Th3: :: HAUSDORF:3 for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) for x being Point of M st x in P holds 0 in (dist x) .: P proofend; theorem Th4: :: HAUSDORF:4 for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) for x being Point of M for y being real number st y in (dist x) .: P holds y >= 0 proofend; theorem Th5: :: HAUSDORF:5 for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) for x being set st x in P holds (dist_min P) . x = 0 proofend; theorem Th6: :: HAUSDORF:6 for M being non empty MetrSpace for p being Point of M for A being Subset of (TopSpaceMetr M) holds ( p in Cl A iff for r being real number st r > 0 holds ex q being Point of M st ( q in A & dist (p,q) < r ) ) proofend; theorem Th7: :: HAUSDORF:7 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) for x being Point of M holds ( (dist_min P) . x = 0 iff for r being real number st r > 0 holds ex p being Point of M st ( p in P & dist (x,p) < r ) ) proofend; theorem Th8: :: HAUSDORF:8 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) for x being Point of M holds ( x in Cl P iff (dist_min P) . x = 0 ) proofend; theorem Th9: :: HAUSDORF:9 for M being non empty MetrSpace for P being non empty closed Subset of (TopSpaceMetr M) for x being Point of M holds ( x in P iff (dist_min P) . x = 0 ) proofend; theorem Th10: :: HAUSDORF:10 for A being non empty Subset of R^1 ex X being non empty Subset of REAL st ( A = X & lower_bound A = lower_bound X ) proofend; theorem Th11: :: HAUSDORF:11 for A being non empty Subset of R^1 ex X being non empty Subset of REAL st ( A = X & upper_bound A = upper_bound X ) proofend; theorem Th12: :: HAUSDORF:12 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 holds X is bounded_below proofend; theorem Th13: :: HAUSDORF:13 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) for x, y being Point of M st y in P holds (dist_min P) . x <= dist (x,y) proofend; theorem Th14: :: HAUSDORF:14 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) for r being real number for x being Point of M st ( for y being Point of M st y in P holds dist (x,y) >= r ) holds (dist_min P) . x >= r proofend; theorem Th15: :: HAUSDORF:15 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) for x, y being Point of M holds (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y) proofend; theorem Th16: :: HAUSDORF:16 for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) for Q being non empty Subset of M st P = Q holds (TopSpaceMetr M) | P = TopSpaceMetr (M | Q) proofend; theorem Th17: :: HAUSDORF:17 for M being non empty MetrSpace for A being Subset of M for B being non empty Subset of M for C being Subset of (M | B) st A = C & C is bounded holds A is bounded proofend; theorem :: HAUSDORF:18 for M being non empty MetrSpace for B being Subset of M for A being Subset of (TopSpaceMetr M) st A = B & A is compact holds B is bounded proofend; theorem Th19: :: HAUSDORF:19 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) for z being Point of M ex w being Point of M st ( w in P & (dist_min P) . z <= dist (w,z) ) proofend; registration let M be non empty MetrSpace; let x be Point of M; cluster dist x -> continuous ; coherence dist x is continuous by WEIERSTR:16; end; registration let M be non empty MetrSpace; let X be non empty compact Subset of (TopSpaceMetr M); cluster dist_max X -> continuous ; coherence dist_max X is continuous by WEIERSTR:24; cluster dist_min X -> continuous ; coherence dist_min X is continuous by WEIERSTR:27; end; 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 proofend; theorem Th20: :: HAUSDORF:20 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) for x, y being Point of M st y in P & P is compact holds (dist_max P) . x >= dist (x,y) proofend; theorem :: HAUSDORF:21 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) for z being Point of M st P is compact holds ex w being Point of M st ( w in P & (dist_max P) . z >= dist (w,z) ) proofend; theorem Th22: :: HAUSDORF:22 for M being non empty MetrSpace for P, Q being non empty Subset of (TopSpaceMetr M) for z being Point of M st P is compact & Q is compact & z in Q holds (dist_min P) . z <= max_dist_max (P,Q) proofend; theorem Th23: :: HAUSDORF:23 for M being non empty MetrSpace for P, Q being non empty Subset of (TopSpaceMetr M) for z being Point of M st P is compact & Q is compact & z in Q holds (dist_max P) . z <= max_dist_max (P,Q) proofend; theorem :: HAUSDORF:24 for M being non empty MetrSpace for P, Q being non empty Subset of (TopSpaceMetr M) for X being Subset of REAL st X = (dist_max P) .: Q & P is compact & Q is compact holds X is bounded_above proofend; theorem Th25: :: HAUSDORF:25 for M being non empty MetrSpace for P, Q being non empty Subset of (TopSpaceMetr M) for X being Subset of REAL st X = (dist_min P) .: Q & P is compact & Q is compact holds X is bounded_above proofend; theorem :: HAUSDORF:26 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) for z being Point of M st P is compact holds (dist_min P) . z <= (dist_max P) . z proofend; theorem Th27: :: HAUSDORF:27 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) holds (dist_min P) .: P = {0} proofend; theorem Th28: :: HAUSDORF:28 for M being non empty MetrSpace for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds max_dist_min (P,Q) >= 0 proofend; theorem Th29: :: HAUSDORF:29 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) holds max_dist_min (P,P) = 0 proofend; theorem :: HAUSDORF:30 for M being non empty MetrSpace for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds min_dist_max (P,Q) >= 0 proofend; theorem Th31: :: HAUSDORF:31 for M being non empty MetrSpace for Q, R being non empty Subset of (TopSpaceMetr M) for y being Point of M st Q is compact & R is compact & y in Q holds (dist_min R) . y <= max_dist_min (R,Q) proofend; begin 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_:_ for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) holds HausDist (P,Q) = max ((max_dist_min (P,Q)),(max_dist_min (Q,P))); theorem Th32: :: HAUSDORF:32 for M being non empty MetrSpace for Q, R being non empty Subset of (TopSpaceMetr M) for y being Point of M st Q is compact & R is compact & y in Q holds (dist_min R) . y <= HausDist (Q,R) proofend; theorem Th33: :: HAUSDORF:33 for M being non empty MetrSpace for P, Q, R being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & R is compact holds max_dist_min (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) proofend; theorem :: HAUSDORF:34 for M being non empty MetrSpace for P, Q, R being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & R is compact holds max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R)) proofend; theorem Th35: :: HAUSDORF:35 for M being non empty MetrSpace for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds HausDist (P,Q) >= 0 proofend; theorem :: HAUSDORF:36 for M being non empty MetrSpace for P being non empty Subset of (TopSpaceMetr M) holds HausDist (P,P) = 0 by Th29; theorem Th37: :: HAUSDORF:37 for M being non empty MetrSpace for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & HausDist (P,Q) = 0 holds P = Q proofend; theorem Th38: :: HAUSDORF:38 for M being non empty MetrSpace for P, Q, R being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & R is compact holds HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) proofend; 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 P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & it = max_dist_min (P9,Q9) ); existence ex b1 being Real ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & b1 = max_dist_min (P9,Q9) ) proofend; uniqueness for b1, b2 being Real st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & b1 = max_dist_min (P9,Q9) ) & ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & b2 = max_dist_min (P9,Q9) ) holds b1 = b2 ; end; :: deftheorem defines max_dist_min HAUSDORF:def_2_:_ for n being Element of NAT for P, Q being Subset of (TOP-REAL n) for b4 being Real holds ( b4 = max_dist_min (P,Q) iff ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & b4 = max_dist_min (P9,Q9) ) ); 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 P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & it = HausDist (P9,Q9) ); existence ex b1 being Real ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & b1 = HausDist (P9,Q9) ) proofend; uniqueness for b1, b2 being Real st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & b1 = HausDist (P9,Q9) ) & ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & b2 = HausDist (P9,Q9) ) holds b1 = b2 ; commutativity for b1 being Real for P, Q being Subset of (TOP-REAL n) st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & b1 = HausDist (P9,Q9) ) holds ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( Q = P9 & P = Q9 & b1 = HausDist (P9,Q9) ) ; end; :: deftheorem Def3 defines HausDist HAUSDORF:def_3_:_ for n being Element of NAT for P, Q being Subset of (TOP-REAL n) for b4 being Real holds ( b4 = HausDist (P,Q) iff ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st ( P = P9 & Q = Q9 & b4 = HausDist (P9,Q9) ) ); theorem :: HAUSDORF:39 for n being Element of NAT for P, Q being non empty Subset of (TOP-REAL n) st P is compact & Q is compact holds HausDist (P,Q) >= 0 proofend; theorem :: HAUSDORF:40 for n being Element of NAT for P being non empty Subset of (TOP-REAL n) holds HausDist (P,P) = 0 proofend; theorem :: HAUSDORF:41 for n being Element of NAT for P, Q being non empty Subset of (TOP-REAL n) st P is compact & Q is compact & HausDist (P,Q) = 0 holds P = Q proofend; theorem :: HAUSDORF:42 for n being Element of NAT for P, Q, R being non empty Subset of (TOP-REAL n) st P is compact & Q is compact & R is compact holds HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) proofend;