The abstract of the Mizar article:

On the Hausdorff Distance Between Compact Subsets

by

Adam Grabowski

Received January 27, 2003

MML identifier: HAUSDORF

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, PRE_TOPC, COMPTS_1, METRIC_1, SUBSET_1, PCOMPS_1, RELAT_1,
      ORDINAL2, SEQ_4, SEQ_2, FUNCT_1, CONNSP_2, TOPS_1, ARYTM_1, HAUSDORF,
      SQUARE_1, WEIERSTR, TOPMETR, LATTICES, TBSP_1, EUCLID, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1, STRUCT_0, PRE_TOPC, TOPS_1,
      COMPTS_1, TBSP_1, TOPMETR, METRIC_1, PCOMPS_1, EUCLID, PSCOMP_1,
      WEIERSTR, CONNSP_2, SEQ_4;
 constructors REAL_1, CONNSP_1, SQUARE_1, PSCOMP_1, TOPS_1, WEIERSTR, COMPTS_1,
      TBSP_1;
 clusters XREAL_0, RELSET_1, SUBSET_1, STRUCT_0, PRE_TOPC, EUCLID, METRIC_1,
      PCOMPS_1, TOPMETR, WAYBEL_2, BORSUK_4, MEMBERED;
 requirements SUBSET, BOOLE, NUMERALS;


begin :: Preliminaries

definition let r be real number; :: repeated from SEQ_4
  redefine func { r } -> Subset of REAL;
end;

definition let M be non empty MetrSpace;
  cluster TopSpaceMetr M -> being_T2;
end;

theorem :: HAUSDORF:1
  for x, y being real number st
      x >= 0 & y >= 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 number 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,
      q being Point of TopSpaceMetr M,
      r being real number st p = q & r > 0 holds
     Ball (p, r) is a_neighborhood of q;

theorem :: HAUSDORF:7
  for M being non empty MetrSpace,
      A being Subset of TopSpaceMetr M,
      p being Point of M holds
     p in Cl A iff
      for r being real number st r > 0 holds Ball (p, r) meets A;

theorem :: HAUSDORF:8
  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 number st r > 0
       ex q being Point of M st q in A & dist (p, q) < r;

theorem :: HAUSDORF:9
  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 number st r > 0
       ex p being Point of M st p in P & dist (x, p) < r;

theorem :: HAUSDORF:10
  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:11
  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:12
  for A being non empty Subset of R^1
   ex X being non empty Subset of REAL st
    A = X & lower_bound A = inf X;

theorem :: HAUSDORF:13
  for A being non empty Subset of R^1
   ex X being non empty Subset of REAL st
    A = X & upper_bound A = sup X;

theorem :: HAUSDORF:14
  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:15
  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:16
  for M being non empty MetrSpace,
      P being non empty Subset of TopSpaceMetr M,
      r being real number,
      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:17
  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:18
  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:19
  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= B & A = C & C is bounded holds A is bounded;

theorem :: HAUSDORF:20
    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:21
  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);

definition let M be non empty MetrSpace, x be Point of M;
  cluster dist x -> continuous;
end;

definition 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:22
  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:23
    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:24
  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:25
  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:26
    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:27
  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:28
    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:29
  for M being non empty MetrSpace,
      P being non empty Subset of TopSpaceMetr M holds
    (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
    max_dist_min (P, Q) >= 0;

theorem :: HAUSDORF:31
  for M being non empty MetrSpace,
      P being non empty Subset of TopSpaceMetr M holds
    max_dist_min (P, P) = 0;

theorem :: HAUSDORF:32
    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:33
  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:34
  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:35
  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:36
  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:37
  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:38
  for M being non empty MetrSpace,
      P being non empty Subset of TopSpaceMetr M holds
    HausDist (P, P) = 0;

theorem :: HAUSDORF:39
  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:40
  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 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');
end;

definition let n be Nat;
           let P, Q be Subset of TOP-REAL n;
  func HausDist (P, Q) -> Real means
:: HAUSDORF:def 3
  ex P', Q' being Subset of TopSpaceMetr Euclid n st
     P = P' & Q = Q' & it = HausDist (P', Q');
  commutativity;
end;

reserve n for Nat;

theorem :: HAUSDORF:41
    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:42
    for P being non empty Subset of TOP-REAL n holds
    HausDist (P, P) = 0;

theorem :: HAUSDORF:43
    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:44
    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);