:: On the {H}ausdorff Distance Between Compact Subsets :: by Adam Grabowski :: :: Received January 27, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, METRIC_1, PCOMPS_1, PRE_TOPC, XXREAL_0, CARD_1, FUNCT_1, SUBSET_1, RELAT_1, STRUCT_0, WEIERSTR, NUMBERS, SEQ_4, ARYTM_3, RCOMP_1, TOPMETR, ORDINAL2, XXREAL_2, ARYTM_1, REAL_1, TARSKI, TBSP_1, EUCLID, HAUSDORF; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, BINOP_1, XXREAL_2, STRUCT_0, PRE_TOPC, COMPTS_1, TBSP_1, TOPMETR, METRIC_1, SEQ_4, PCOMPS_1, EUCLID, WEIERSTR; constructors REAL_1, SQUARE_1, SEQ_4, CONNSP_1, COMPTS_1, TBSP_1, WEIERSTR, FUNCSDOM, BINOP_2, PSCOMP_1; registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, PCOMPS_1, EUCLID, TOPMETR, BORSUK_2, WAYBEL_2, TBSP_1, VALUED_0; requirements SUBSET, BOOLE; begin :: Preliminaries registration let M be non empty MetrSpace; cluster TopSpaceMetr M -> T_2; end; theorem :: HAUSDORF:1 for x, y being Real st x >= 0 & max (x,y) = 0 holds x = 0; theorem :: HAUSDORF:2 for M being non empty MetrSpace, x being Point of M holds (dist x ) . x = 0; theorem :: HAUSDORF:3 for M being non empty MetrSpace, P being Subset of TopSpaceMetr M , x being Point of M st x in P holds 0 in (dist x) .: P; theorem :: HAUSDORF:4 for M being non empty MetrSpace, P being Subset of TopSpaceMetr M , x being Point of M, y being Real st y in (dist x) .: P holds y >= 0; theorem :: HAUSDORF:5 for M being non empty MetrSpace, P being Subset of TopSpaceMetr M , x being set st x in P holds (dist_min P) . x = 0; theorem :: HAUSDORF:6 for M being non empty MetrSpace, p being Point of M, A being Subset of TopSpaceMetr M holds p in Cl A iff for r being Real st r > 0 ex q being Point of M st q in A & dist (p, q) < r; theorem :: HAUSDORF:7 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M, x being Point of M holds (dist_min P) . x = 0 iff for r being Real st r > 0 ex p being Point of M st p in P & dist (x, p) < r; theorem :: HAUSDORF:8 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M, x being Point of M holds x in Cl P iff (dist_min P) . x = 0; theorem :: HAUSDORF:9 for M being non empty MetrSpace, P being non empty closed Subset of TopSpaceMetr M, x being Point of M holds x in P iff (dist_min P) . x = 0; theorem :: 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; theorem :: 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; theorem :: HAUSDORF:12 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M, x being Point of M, X being Subset of REAL st X = (dist x) .: P holds X is bounded_below; theorem :: HAUSDORF:13 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M, x, y being Point of M st y in P holds (dist_min P) . x <= dist (x, y); theorem :: HAUSDORF:14 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M, r being Real, x being Point of M holds (for y being Point of M st y in P holds dist (x,y) >= r) implies (dist_min P) . x >= r; theorem :: HAUSDORF:15 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M, x, y being Point of M holds (dist_min P) . x <= dist (x, y) + ( dist_min P) . y; theorem :: HAUSDORF:16 for M being non empty MetrSpace, P being Subset of TopSpaceMetr M, Q being non empty Subset of M holds P = Q implies (TopSpaceMetr M)|P = TopSpaceMetr(M|Q); theorem :: HAUSDORF:17 for M being non empty MetrSpace, A being Subset of M, B being non empty Subset of M, C being Subset of M|B st A = C & C is bounded holds A is bounded; theorem :: HAUSDORF:18 for M being non empty MetrSpace, B being Subset of M, A being Subset of TopSpaceMetr M st A = B & A is compact holds B is bounded; theorem :: HAUSDORF:19 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M, z being Point of M holds ex w being Point of M st w in P & ( dist_min P) . z <= dist (w, z); registration let M be non empty MetrSpace, x be Point of M; cluster dist x -> continuous; end; registration let M be non empty MetrSpace, X be compact non empty Subset of TopSpaceMetr M; cluster dist_max X -> continuous; cluster dist_min X -> continuous; end; theorem :: HAUSDORF:20 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M, x, y being Point of M st y in P & P is compact holds (dist_max P) . x >= dist (x, y); theorem :: HAUSDORF:21 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M, 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); theorem :: HAUSDORF:22 for M being non empty MetrSpace, P, Q being non empty Subset of TopSpaceMetr M, 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); theorem :: HAUSDORF:23 for M being non empty MetrSpace, P, Q being non empty Subset of TopSpaceMetr M, 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); theorem :: HAUSDORF:24 for M being non empty MetrSpace, P, Q being non empty Subset of TopSpaceMetr M, X being Subset of REAL st X = (dist_max P) .: Q & P is compact & Q is compact holds X is bounded_above; theorem :: HAUSDORF:25 for M being non empty MetrSpace, P, Q being non empty Subset of TopSpaceMetr M, X being Subset of REAL st X = (dist_min P) .: Q & P is compact & Q is compact holds X is bounded_above; theorem :: HAUSDORF:26 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M, z being Point of M st P is compact holds (dist_min P) . z <= ( dist_max P) . z; theorem :: HAUSDORF:27 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M holds (dist_min P) .: P = { 0 }; theorem :: HAUSDORF:28 for M being non empty MetrSpace, P, Q being non empty Subset of TopSpaceMetr M st P is compact & Q is compact holds max_dist_min (P, Q) >= 0; theorem :: HAUSDORF:29 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M holds max_dist_min (P, P) = 0; theorem :: HAUSDORF:30 for M being non empty MetrSpace, P, Q being non empty Subset of TopSpaceMetr M st P is compact & Q is compact holds min_dist_max (P, Q) >= 0; theorem :: HAUSDORF:31 for M being non empty MetrSpace, Q, R being non empty Subset of TopSpaceMetr M, 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); begin :: Hausdorff Distance definition let M be non empty MetrSpace, 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) ); commutativity; end; theorem :: HAUSDORF:32 for M being non empty MetrSpace, Q, R being non empty Subset of TopSpaceMetr M, y being Point of M st Q is compact & R is compact & y in Q holds (dist_min R).y <= HausDist (Q, R); theorem :: HAUSDORF:33 for M being non empty MetrSpace, 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); theorem :: HAUSDORF:34 for M being non empty MetrSpace, 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); theorem :: HAUSDORF:35 for M being non empty MetrSpace, P, Q being non empty Subset of TopSpaceMetr M st P is compact & Q is compact holds HausDist (P, Q) >= 0; theorem :: HAUSDORF:36 for M being non empty MetrSpace, P being non empty Subset of TopSpaceMetr M holds HausDist (P, P) = 0; theorem :: HAUSDORF:37 for M being non empty MetrSpace, P, Q being non empty Subset of TopSpaceMetr M st P is compact & Q is compact & HausDist (P, Q) = 0 holds P = Q ; theorem :: HAUSDORF:38 for M being non empty MetrSpace, 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); 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); end; definition let n be Element of NAT; let P, Q be Subset of TOP-REAL n; func HausDist (P, Q) -> Real means :: HAUSDORF:def 3 ex P9, Q9 being Subset of TopSpaceMetr Euclid n st P = P9 & Q = Q9 & it = HausDist (P9, Q9); commutativity; end; reserve n for Element of NAT; theorem :: HAUSDORF:39 for P, Q being non empty Subset of TOP-REAL n st P is compact & Q is compact holds HausDist (P, Q) >= 0; theorem :: HAUSDORF:40 for P being non empty Subset of TOP-REAL n holds HausDist (P, P) = 0; theorem :: HAUSDORF:41 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; theorem :: HAUSDORF:42 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);