:: On the {H}ausdorff Distance Between Compact Subsets
::  by Adam Grabowski
::
:: Received January 27, 2003
:: Copyright (c) 2003-2012 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, XREAL_0, ORDINAL1,
      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, XREAL_0,
      REAL_1, SQUARE_1, FUNCT_1, RELSET_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;
 definitions XBOOLE_0, TARSKI, STRUCT_0, XXREAL_2;
 theorems METRIC_1, TOPMETR, GOBOARD6, PRE_TOPC, FUNCT_2, XBOOLE_0, FUNCT_1,
      TARSKI, WEIERSTR, SEQ_4, TBSP_1, JORDAN1K, COMPTS_1, PCOMPS_1, XREAL_1,
      XXREAL_0, XXREAL_2, EUCLID;

begin :: Preliminaries

registration
  let M be non empty MetrSpace;
  cluster TopSpaceMetr M -> T_2;
  coherence by PCOMPS_1:34;
end;

theorem Th1:
  for x, y being real number st x >= 0 & max (x,y) = 0 holds x = 0
proof
  let x, y be real number;
  assume that
A1: x >= 0 and
A2: max (x,y) = 0;
  per cases by XXREAL_0:16;
  suppose
    max (x,y) = x;
    hence thesis by A2;
  end;
  suppose
A3: max (x,y) = y;
    then x <= y by XXREAL_0:25;
    hence thesis by A1,A2,A3,XXREAL_0:1;
  end;
end;

theorem Th2:
  for M being non empty MetrSpace, x being Point of M holds (dist x ) . x = 0
proof
  let M be non empty MetrSpace, x be Point of M;
  (dist x).x = dist (x, x) by WEIERSTR:def 4
    .= 0 by METRIC_1:1;
  hence thesis;
end;

theorem Th3:
  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
proof
  let M be non empty MetrSpace, P be Subset of TopSpaceMetr M, x be Point of M;
A1: dom dist x = the carrier of TopSpaceMetr M by FUNCT_2:def 1;
  assume x in P;
  then (dist x).x in ((dist x) .: P) by A1,FUNCT_1:def 6;
  hence thesis by Th2;
end;

theorem Th4:
  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
proof
  let M be non empty MetrSpace, P be Subset of TopSpaceMetr M, x be Point of M
  , y be real number;
  assume y in (dist x) .: P;
  then consider z being set such that
  z in dom dist x and
A1: z in P and
A2: y = (dist x).z by FUNCT_1:def 6;
  reconsider z9 = z as Point of M by A1,TOPMETR:12;
  y = dist (x, z9) by A2,WEIERSTR:def 4;
  hence thesis by METRIC_1:5;
end;

theorem Th5:
  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
proof
  let M be non empty MetrSpace, P be Subset of TopSpaceMetr M, x be set;
  assume
A1: x in P;
  then reconsider x as Point of M by TOPMETR:12;
  set X = (dist x) .: P;
  reconsider X as non empty Subset of REAL by A1,TOPMETR:17;
  lower_bound ((dist x) .: P) = lower_bound [#] ((dist x) .: P) by
WEIERSTR:def 3
    .= lower_bound X by WEIERSTR:def 1;
  then
A2: (dist_min P) . x = lower_bound X by WEIERSTR:def 6;
A3: for p being real number st p in X holds p >= 0 by Th4;
  for q being real number st for p being real number st p in X holds p >=
  q holds 0 >= q by A1,Th3;
  hence thesis by A2,A3,SEQ_4:44;
end;

theorem Th6:
  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
proof
  let M be non empty MetrSpace, p be Point of M, A be Subset of TopSpaceMetr M;
  hereby
    assume
A1: p in Cl A;
    let r be real number;
    assume r > 0;
    then Ball (p, r) meets A by A1,GOBOARD6:92;
    then consider x being set such that
A2: x in Ball (p, r) and
A3: x in A by XBOOLE_0:3;
    reconsider q = x as Point of M by A2;
    take q;
    thus q in A by A3;
    thus dist (p, q) < r by A2,METRIC_1:11;
  end;
  assume
A4: for r being real number st r > 0 ex q being Point of M st q in A &
  dist (p, q) < r;
  for r being real number st r > 0 holds Ball (p, r) meets A
  proof
    let r be real number;
    assume r > 0;
    then consider q being Point of M such that
A5: q in A and
A6: dist (p, q) < r by A4;
    q in Ball (p, r) by A6,METRIC_1:11;
    hence thesis by A5,XBOOLE_0:3;
  end;
  hence thesis by GOBOARD6:92;
end;

theorem Th7:
  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
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, x be
  Point of M;
  reconsider X = (dist(x)).:P as non empty Subset of REAL by TOPMETR:17;
  hereby
    assume
A1: (dist_min P) . x = 0;
    let r be real number;
    assume
A2: r > 0;
    assume
A3: for p being Point of M st p in P holds dist (x, p) >= r;
    for p being real number st p in X holds p >= r
    proof
      let p be real number;
      assume p in X;
      then consider y being set such that
A4:   y in dom dist x and
A5:   y in P and
A6:   p = (dist x).y by FUNCT_1:def 6;
      reconsider z = y as Point of M by A4,TOPMETR:12;
      dist (x, z) >= r by A3,A5;
      hence thesis by A6,WEIERSTR:def 4;
    end;
    then
A7: lower_bound X >= r by SEQ_4:43;
    lower_bound ((dist x) .: P) = lower_bound [#] ((dist x) .: P) by
WEIERSTR:def 3
      .= lower_bound X by WEIERSTR:def 1;
    hence contradiction by A1,A2,A7,WEIERSTR:def 6;
  end;
A8: for p being real number st p in X holds p >= 0
  proof
    let p be real number;
    assume p in X;
    then consider y being set such that
A9: y in dom dist x and
    y in P and
A10: p = (dist x).y by FUNCT_1:def 6;
    reconsider z = y as Point of M by A9,TOPMETR:12;
    dist (x, z) >= 0 by METRIC_1:5;
    hence thesis by A10,WEIERSTR:def 4;
  end;
  assume
A11: for r being real number st r > 0 ex p being Point of M st p in P &
  dist (x, p) < r;
A12: for q being real number st for p being real number st p in X holds p >=
  q holds 0 >= q
  proof
    let q be real number;
    assume
A13: for z being real number st z in X holds z >= q;
    assume 0 < q;
    then consider p being Point of M such that
A14: p in P and
A15: dist (x, p) < q by A11;
    set z = (dist x).p;
    p in the carrier of TopSpaceMetr M by A14;
    then p in dom dist x by FUNCT_2:def 1;
    then
A16: z in X by A14,FUNCT_1:def 6;
    (dist x).p < q by A15,WEIERSTR:def 4;
    hence thesis by A13,A16;
  end;
  lower_bound ((dist x) .: P) = lower_bound [#] ((dist x) .: P) by
WEIERSTR:def 3
    .= lower_bound X by WEIERSTR:def 1;
  then lower_bound((dist(x)).:P) = 0 by A8,A12,SEQ_4:44;
  hence thesis by WEIERSTR:def 6;
end;

theorem Th8:
  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
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, x be
  Point of M;
  hereby
    assume x in Cl P;
    then for a being real number st a > 0 ex p being Point of M st p in P &
    dist (x, p) < a by Th6;
    hence (dist_min P) . x = 0 by Th7;
  end;
  assume (dist_min P) . x = 0;
  then
  for a being real number st a > 0 ex p being Point of M st p in P & dist
  (x, p) < a by Th7;
  hence thesis by Th6;
end;

theorem Th9:
  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
proof
  let M be non empty MetrSpace, P be non empty closed Subset of TopSpaceMetr M
  , x be Point of M;
  P = Cl P by PRE_TOPC:22;
  hence thesis by Th8;
end;

theorem Th10:
  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
proof
  let A be non empty Subset of R^1;
  reconsider X = A as non empty Subset of REAL by TOPMETR:17;
  take X;
  lower_bound A = lower_bound [#] A by WEIERSTR:def 3
    .= lower_bound X by WEIERSTR:def 1;
  hence thesis;
end;

theorem Th11:
  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
proof
  let A be non empty Subset of R^1;
  reconsider X = A as non empty Subset of REAL by TOPMETR:17;
  take X;
  upper_bound A = upper_bound [#] A by WEIERSTR:def 2
    .= upper_bound X by WEIERSTR:def 1;
  hence thesis;
end;

theorem Th12:
  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
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, x be
  Point of M, X be Subset of REAL;
  assume
A1: X = (dist x).:P;
  take 0;
  let y be ext-real number;
  thus y in X implies 0 <= y by A1,Th4;
end;

theorem Th13:
  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)
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, x, y
  be Point of M;
A1: dom dist x = the carrier of TopSpaceMetr M & dist (x, y) = (dist x).y by
FUNCT_2:def 1,WEIERSTR:def 4;
  consider X being non empty Subset of REAL such that
A2: X = (dist x) .: P and
A3: lower_bound ((dist x).:P) = lower_bound X by Th10;
  assume y in P;
  then
A4: dist (x, y) in X by A2,A1,FUNCT_1:def 6;
  (dist_min P) . x = lower_bound X & X is bounded_below
   by A2,A3,Th12,WEIERSTR:def 6;
  hence thesis by A4,SEQ_4:def 2;
end;

theorem Th14:
  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
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, r be
  real number, x be Point of M;
  consider X being non empty Subset of REAL such that
A1: X = (dist x).:P and
A2: lower_bound ((dist x).:P) = lower_bound X by Th10;
  assume
A3: for y being Point of M st y in P holds dist (x,y) >= r;
  for p being real number st p in X holds p >= r
  proof
    let p be real number;
    assume p in X;
    then consider y being set such that
A4: y in dom dist x and
A5: y in P and
A6: (dist x).y = p by A1,FUNCT_1:def 6;
    reconsider y as Point of M by A4,TOPMETR:12;
    p = dist (x, y) by A6,WEIERSTR:def 4;
    hence thesis by A3,A5;
  end;
  then lower_bound X >= r by SEQ_4:43;
  hence thesis by A2,WEIERSTR:def 6;
end;

theorem Th15:
  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
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, x, y
  be Point of M;
  now
    let z be Point of M;
    assume z in P;
    then (dist_min P) . x <= dist (x, z) by Th13;
    then
A1: dist (x, z) - dist (x, y) >= (dist_min P) . x - dist (x, y) by XREAL_1:13;
    dist (x, z) <= dist (x, y) + dist (y, z) by METRIC_1:4;
    then dist (y, z) >= dist (x, z) - dist (x, y) by XREAL_1:20;
    hence dist (y, z) >= (dist_min P) . x - dist (x, y) by A1,XXREAL_0:2;
  end;
  then (dist_min P) . y >= (dist_min P) . x - dist (x, y) by Th14;
  hence thesis by XREAL_1:20;
end;

theorem Th16:
  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)
proof
  let M be non empty MetrSpace, P be Subset of TopSpaceMetr M, Q be non empty
  Subset of M;
  reconsider N = TopSpaceMetr(M|Q) as SubSpace of TopSpaceMetr M by TOPMETR:13;
A1: the carrier of N = the carrier of M|Q by TOPMETR:12;
  assume P = Q;
  then [#]N = P by A1,TOPMETR:def 2;
  hence thesis by PRE_TOPC:def 5;
end;

theorem Th17:
  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
proof
  let M be non empty MetrSpace, A be Subset of M, B be non empty Subset of M,
  C be Subset of M|B;
  assume that
A1: A = C and
A2: C is bounded;
  consider r0 being Real such that
A3: 0 < r0 and
A4: for x, y being Point of M|B st x in C & y in C holds dist(x,y) <= r0
  by A2,TBSP_1:def 7;
  for x, y being Point of M st x in A & y in A holds dist(x,y) <= r0
  proof
    let x, y be Point of M;
    assume
A5: x in A & y in A;
    then reconsider x0 = x, y0 = y as Point of M|B by A1;
A6: (the distance of (M|B)).(x0,y0) = (the distance of M).(x,y) & (the
    distance of (M|B)).(x0,y0) = dist(x0,y0) by METRIC_1:def 1,TOPMETR:def 1;
    dist(x0,y0) <= r0 by A1,A4,A5;
    hence thesis by A6,METRIC_1:def 1;
  end;
  hence thesis by A3,TBSP_1:def 7;
end;

theorem
  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
proof
  let M be non empty MetrSpace, B be Subset of M, A be Subset of TopSpaceMetr
  M;
  set TA = TopSpaceMetr M;
  assume that
A1: A = B and
A2: A is compact;
  A c= the carrier of (TA|A) by PRE_TOPC:8;
  then reconsider A2 = A as Subset of (TA|A);
  per cases;
  suppose
    A <> {};
    then reconsider A1 = A as non empty Subset of M by TOPMETR:12;
    [#](TA|A) = A2 by PRE_TOPC:def 5;
    then [#](TA|A) is compact by A2,COMPTS_1:2;
    then
A3: TA|A is compact by COMPTS_1:1;
    TopSpaceMetr (M|A1) = TA|A by Th16;
    then M|A1 is totally_bounded by A3,TBSP_1:9;
    then M|A1 is bounded by TBSP_1:19;
    then
A4: [#](M|A1) is bounded;
    [#](M|A1) = the carrier of M|A1 .= A1 by TOPMETR:def 2;
    hence thesis by A1,A4,Th17;
  end;
  suppose
    A = {};
    then A = {} M;
    hence thesis by A1;
  end;
end;

theorem Th19:
  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)
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, z be
  Point of M;
  consider w being set such that
A1: w in P by XBOOLE_0:def 1;
  reconsider w as Point of M by A1,TOPMETR:12;
  take w;
  thus w in P by A1;
  thus thesis by A1,Th13;
end;

registration
  let M be non empty MetrSpace, x be Point of M;
  cluster dist x -> continuous;
  coherence by WEIERSTR:16;
end;

registration
  let M be non empty MetrSpace, X be compact non empty Subset of TopSpaceMetr
  M;
  cluster dist_max X -> continuous;
  coherence by WEIERSTR:24;
  cluster dist_min X -> continuous;
  coherence by WEIERSTR:27;
end;

Lm1: 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 & P is
compact holds X is bounded_above
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, x be
  Point of M, X be Subset of REAL;
  assume X = (dist x) .: P & P is compact;
  then [#]((dist x) .: P) is real-bounded & X = [#]((dist x) .: P)
  by WEIERSTR:9,11,def 1;
  hence thesis by XXREAL_2:def 11;
end;

theorem Th20:
  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)
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, x, y
  be Point of M;
  assume that
A1: y in P and
A2: P is compact;
  consider X being non empty Subset of REAL such that
A3: X = (dist x) .: P and
A4: upper_bound ((dist x).:P) = upper_bound X by Th11;
A5: (dist_max P) . x = upper_bound X by A4,WEIERSTR:def 5;
  dom dist x = the carrier of TopSpaceMetr M & dist (x, y) = (dist x).y by
FUNCT_2:def 1,WEIERSTR:def 4;
  then
A6: dist (x, y) in X by A1,A3,FUNCT_1:def 6;
  X is bounded_above by A2,A3,Lm1;
  hence thesis by A5,A6,SEQ_4:def 1;
end;

theorem
  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)
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, z be
  Point of M;
  assume
A1: P is compact;
  consider w being set such that
A2: w in P by XBOOLE_0:def 1;
  reconsider w as Point of M by A2,TOPMETR:12;
  take w;
  thus w in P by A2;
  thus thesis by A1,A2,Th20;
end;

theorem Th22:
  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)
proof
  let M be non empty MetrSpace, P, Q be non empty Subset of TopSpaceMetr M, z
  be Point of M;
  consider w being Point of M such that
A1: w in P and
A2: (dist_min P) . z <= dist (w, z) by Th19;
  assume P is compact & Q is compact & z in Q;
  then dist (w, z) <= max_dist_max (P, Q) by A1,WEIERSTR:34;
  hence thesis by A2,XXREAL_0:2;
end;

theorem Th23:
  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)
proof
  let M be non empty MetrSpace, P, Q be non empty Subset of TopSpaceMetr M, z
  be Point of M;
  assume that
A1: P is compact and
A2: Q is compact;
  reconsider P as non empty compact Subset of TopSpaceMetr M by A1;
  set A = (dist_max P) .: Q;
A3: dom dist_max P = the carrier of TopSpaceMetr M by FUNCT_2:def 1;
  assume z in Q;
  then
A4: (dist_max P) . z in A by A3,FUNCT_1:def 6;
  upper_bound ((dist_max P) .: Q) = max_dist_max (P, Q) by WEIERSTR:def 10;
  then consider X being non empty Subset of REAL such that
A5: A = X and
A6: max_dist_max (P, Q) = upper_bound X by Th11;
  [#]A is real-bounded by A2,WEIERSTR:9,11;
  then X is real-bounded by A5,WEIERSTR:def 1;
  then X is bounded_above by XXREAL_2:def 11;
  hence thesis by A5,A6,A4,SEQ_4:def 1;
end;

theorem
  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
proof
  let M be non empty MetrSpace, P, Q be non empty Subset of TopSpaceMetr M, X
  be Subset of REAL;
  assume that
A1: X = (dist_max P).:Q and
A2: P is compact & Q is compact;
  reconsider Q9 = Q as non empty Subset of M by TOPMETR:12;
  X is bounded_above
  proof
    take r = max_dist_max (P, Q);
    let p be ext-real number;
    assume p in X;
    then consider z being set such that
    z in dom dist_max P and
A3: z in Q and
A4: p = (dist_max P).z by A1,FUNCT_1:def 6;
    z in Q9 by A3;
    then reconsider z as Point of M;
    (dist_max P) . z <= r by A2,A3,Th23;
    hence thesis by A4;
  end;
  hence thesis;
end;

theorem Th25:
  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
proof
  let M be non empty MetrSpace, P, Q be non empty Subset of TopSpaceMetr M, X
  be Subset of REAL;
  assume that
A1: X = (dist_min P).:Q and
A2: P is compact & Q is compact;
  reconsider Q9 = Q as non empty Subset of M by TOPMETR:12;
  X is bounded_above
  proof
    take r = max_dist_max (P, Q);
    let p be ext-real number;
    assume p in X;
    then consider z being set such that
    z in dom dist_min P and
A3: z in Q and
A4: p = (dist_min P).z by A1,FUNCT_1:def 6;
    z in Q9 by A3;
    then reconsider z as Point of M;
    (dist_min P) . z <= r by A2,A3,Th22;
    hence thesis by A4;
  end;
  hence thesis;
end;

theorem
  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
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M, z be
  Point of M;
  consider w being Point of M such that
A1: w in P and
A2: (dist_min P) . z <= dist (w, z) by Th19;
  assume P is compact;
  then (dist_max P) . z >= dist (z, w) by A1,Th20;
  hence thesis by A2,XXREAL_0:2;
end;

theorem Th27:
  for M being non empty MetrSpace, P being non empty Subset of
  TopSpaceMetr M holds (dist_min P) .: P = { 0 }
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M;
  consider x being set such that
A1: x in P by XBOOLE_0:def 1;
  thus (dist_min P) .: P c= { 0 }
  proof
    let y be set;
    assume y in (dist_min P) .: P;
    then
    ex x being set st x in dom dist_min P & x in P & y = ( dist_min P).x by
FUNCT_1:def 6;
    then y = 0 by Th5;
    hence thesis by TARSKI:def 1;
  end;
  let y be set;
A2: dom dist_min P = the carrier of TopSpaceMetr M by FUNCT_2:def 1;
  assume y in { 0 };
  then y = 0 by TARSKI:def 1;
  then y = (dist_min P).x by A1,Th5;
  hence thesis by A1,A2,FUNCT_1:def 6;
end;

theorem Th28:
  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
proof
  let M be non empty MetrSpace, P, Q be non empty Subset of TopSpaceMetr M;
  assume P is compact & Q is compact;
  then ex x1, x2 being Point of M st x1 in P & x2 in Q & dist( x1,x2) =
  max_dist_min(P,Q) by WEIERSTR:32;
  hence thesis by METRIC_1:5;
end;

theorem Th29:
  for M being non empty MetrSpace, P being non empty Subset of
  TopSpaceMetr M holds max_dist_min (P, P) = 0
proof
  let M be non empty MetrSpace, P be non empty Subset of TopSpaceMetr M;
A1: [#] ((dist_min P).:P) = (dist_min P) .: P by WEIERSTR:def 1
    .= { 0 } by Th27;
  max_dist_min (P, P) = upper_bound ((dist_min P).:P) by WEIERSTR:def 8
    .= upper_bound { 0 } by A1,WEIERSTR:def 2;
  hence thesis by SEQ_4:9;
end;

theorem
  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
proof
  let M be non empty MetrSpace, P, Q be non empty Subset of TopSpaceMetr M;
  assume P is compact & Q is compact;
  then ex x1, x2 being Point of M st x1 in P & x2 in Q & dist( x1,x2) =
  min_dist_max (P,Q) by WEIERSTR:31;
  hence thesis by METRIC_1:5;
end;

theorem Th31:
  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)
proof
  let M be non empty MetrSpace, Q, R be non empty Subset of TopSpaceMetr M, y
  be Point of M;
  assume that
A1: Q is compact & R is compact and
A2: y in Q;
  set A = (dist_min R) .: Q;
  consider X being non empty Subset of REAL such that
A3: A = X and
A4: upper_bound A = upper_bound X by Th11;
  dom dist_min R = the carrier of TopSpaceMetr M by FUNCT_2:def 1;
  then
A5: (dist_min R).y in X by A2,A3,FUNCT_1:def 6;
  max_dist_min (R, Q) = upper_bound ((dist_min R) .: Q) & X is
  bounded_above by A1,A3,Th25,WEIERSTR:def 8;
  hence thesis by A4,A5,SEQ_4:def 1;
end;

begin :: Hausdorff Distance

definition
  let M be non empty MetrSpace, P, Q be Subset of TopSpaceMetr M;
  func HausDist (P, Q) -> Real equals
  max ( max_dist_min (P, Q), max_dist_min
  (Q, P) );
  coherence;
  commutativity;
end;

theorem Th32:
  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)
proof
  let M be non empty MetrSpace, Q, R be non empty Subset of TopSpaceMetr M, y
  be Point of M;
  assume Q is compact & R is compact & y in Q;
  then
  max_dist_min (R, Q) <= max (max_dist_min (R, Q), max_dist_min (Q, R)) &
  ( dist_min R).y <= max_dist_min (R, Q) by Th31,XXREAL_0:25;
  hence thesis by XXREAL_0:2;
end;

theorem Th33:
  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)
proof
  let M be non empty MetrSpace, P, Q, R be non empty Subset of TopSpaceMetr M;
  assume that
A1: P is compact and
A2: Q is compact and
A3: R is compact;
  reconsider DPR = (dist_min P) .: R as non empty Subset of REAL by TOPMETR:17;
A4: for w being real number st w in DPR holds w <= HausDist (P, Q) +
  HausDist (Q, R)
  proof
    let w be real number;
    assume w in DPR;
    then consider y being set such that
    y in dom dist_min P and
A5: y in R and
A6: w = (dist_min P).y by FUNCT_1:def 6;
    reconsider y as Point of M by A5,TOPMETR:12;
    for z being Point of M st z in Q holds dist (y, z) >= (dist_min P).y -
    HausDist (Q, P)
    proof
      let z be Point of M;
      assume z in Q;
      then (dist_min P).z <= HausDist (Q, P) by A1,A2,Th32;
      then
A7:   dist (y, z) + (dist_min P).z <= dist (y, z) + HausDist (Q, P) by
XREAL_1:6;
      (dist_min P).y <= dist (y, z) + (dist_min P).z by Th15;
      then (dist_min P).y <= dist (y, z) + HausDist (Q, P) by A7,XXREAL_0:2;
      hence thesis by XREAL_1:20;
    end;
    then (dist_min P).y - HausDist (Q, P) <= (dist_min Q).y by Th14;
    then
A8: (dist_min P).y <= HausDist (Q, P) + (dist_min Q).y by XREAL_1:20;
    (dist_min Q).y <= HausDist (R, Q) by A2,A3,A5,Th32;
    then
    HausDist (Q, P) + (dist_min Q).y <= HausDist (Q, P) + HausDist (Q, R)
    by XREAL_1:6;
    hence thesis by A6,A8,XXREAL_0:2;
  end;
  upper_bound DPR = upper_bound [#]((dist_min P).:R) by WEIERSTR:def 1
    .= upper_bound ((dist_min P).:R) by WEIERSTR:def 2
    .= max_dist_min (P, R) by WEIERSTR:def 8;
  hence thesis by A4,SEQ_4:45;
end;

theorem
  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)
proof
  let M be non empty MetrSpace, P, Q, R be non empty Subset of TopSpaceMetr M;
  assume that
A1: P is compact and
A2: Q is compact and
A3: R is compact;
  reconsider DPR = (dist_min R).:P as non empty Subset of REAL by TOPMETR:17;
A4: for w being real number st w in DPR holds w <= HausDist (P, Q) +
  HausDist (Q, R)
  proof
    let w be real number;
    assume w in DPR;
    then consider y being set such that
    y in dom dist_min R and
A5: y in P and
A6: w = (dist_min R).y by FUNCT_1:def 6;
    reconsider y as Point of M by A5,TOPMETR:12;
    for z being Point of M st z in Q holds dist (y, z) >= (dist_min R).y -
    HausDist (Q, R)
    proof
      let z be Point of M;
      assume z in Q;
      then (dist_min R).z <= HausDist (Q, R) by A2,A3,Th32;
      then
A7:   dist (y, z) + (dist_min R).z <= dist (y, z) + HausDist (Q, R) by
XREAL_1:6;
      (dist_min R).y <= dist (y, z) + (dist_min R).z by Th15;
      then (dist_min R).y <= dist (y, z) + HausDist (Q, R) by A7,XXREAL_0:2;
      hence thesis by XREAL_1:20;
    end;
    then
A8: (dist_min R).y - HausDist (Q, R) <= (dist_min Q).y by Th14;
    (dist_min Q).y <= HausDist (P, Q) by A1,A2,A5,Th32;
    then (dist_min R).y - HausDist (Q, R) <= HausDist (P, Q) by A8,XXREAL_0:2;
    hence thesis by A6,XREAL_1:20;
  end;
  upper_bound DPR = upper_bound [#]((dist_min R).:P) by WEIERSTR:def 1
    .= upper_bound ((dist_min R).:P) by WEIERSTR:def 2
    .= max_dist_min (R, P) by WEIERSTR:def 8;
  hence thesis by A4,SEQ_4:45;
end;

theorem Th35:
  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
proof
  let M be non empty MetrSpace, P, Q be non empty Subset of TopSpaceMetr M;
  assume
A1: P is compact & Q is compact;
  per cases by XXREAL_0:16;
  suppose
    HausDist (P, Q) = max_dist_min (P, Q);
    hence thesis by A1,Th28;
  end;
  suppose
    HausDist (P, Q) = max_dist_min (Q, P);
    hence thesis by A1,Th28;
  end;
end;

theorem
  for M being non empty MetrSpace, P being non empty Subset of
  TopSpaceMetr M holds HausDist (P, P) = 0 by Th29;

theorem Th37:
  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
proof
  let M be non empty MetrSpace, P, Q be non empty Subset of TopSpaceMetr M;
  assume that
A1: P is compact and
A2: Q is compact;
A3: Q is closed by A2,COMPTS_1:7;
  assume
A4: HausDist (P, Q) = 0;
  then max_dist_min (Q, P) = 0 by A1,A2,Th1,Th28;
  then upper_bound ((dist_min Q).:P) = 0 by WEIERSTR:def 8;
  then consider Y being non empty Subset of REAL such that
A5: (dist_min Q) .: P = Y and
A6: 0 = upper_bound Y by Th11;
A7: Y is bounded_above by A1,A2,A5,Th25;
  thus P c= Q
  proof
    let x be set;
    assume
A8: x in P;
    then reconsider x9 = x as Point of M by TOPMETR:12;
    dom dist_min Q = the carrier of TopSpaceMetr M by FUNCT_2:def 1;
    then (dist_min Q) . x in Y by A5,A8,FUNCT_1:def 6;
    then
A9: (dist_min Q) . x <= 0 by A6,A7,SEQ_4:def 1;
    (dist_min Q) . x >= 0 by A8,JORDAN1K:9;
    then (dist_min Q) . x = 0 by A9,XXREAL_0:1;
    then x9 in Q by A3,Th9;
    hence thesis;
  end;
  let x be set;
  assume
A10: x in Q;
  then reconsider x9 = x as Point of M by TOPMETR:12;
A11: P is closed by A1,COMPTS_1:7;
  max_dist_min (P, Q) = 0 by A1,A2,A4,Th1,Th28;
  then upper_bound ((dist_min P).:Q) = 0 by WEIERSTR:def 8;
  then consider X being non empty Subset of REAL such that
A12: (dist_min P) .: Q = X and
A13: 0 = upper_bound X by Th11;
  dom dist_min P = the carrier of TopSpaceMetr M by FUNCT_2:def 1;
  then
A14: (dist_min P) . x in X by A12,A10,FUNCT_1:def 6;
  X is bounded_above by A1,A2,A12,Th25;
  then
A15: (dist_min P) . x <= 0 by A13,A14,SEQ_4:def 1;
  (dist_min P) . x >= 0 by A10,JORDAN1K:9;
  then (dist_min P) . x = 0 by A15,XXREAL_0:1;
  then x9 in P by A11,Th9;
  hence thesis;
end;

theorem Th38:
  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)
proof
  let M be non empty MetrSpace, P, Q, R be non empty Subset of TopSpaceMetr M;
  assume P is compact & Q is compact & R is compact;
  then
  max_dist_min (P, R) <= HausDist (P, Q) + HausDist (Q, R) & max_dist_min
  (R, P) <= HausDist (P, Q) + HausDist (Q, R) by Th33;
  hence thesis by XXREAL_0:28;
end;

definition
  let n be Element of NAT;
  let P, Q be Subset of TOP-REAL n;
  func max_dist_min (P, Q) -> Real means
  ex P9, Q9 being Subset of
  TopSpaceMetr Euclid n st P = P9 & Q = Q9 & it = max_dist_min (P9, Q9);
  existence
  proof
    the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
    then reconsider P9 = P, Q9 = Q as Subset of TopSpaceMetr Euclid n;
    take max_dist_min(P9,Q9), P9, Q9;
    thus thesis;
  end;
  uniqueness;
end;

definition
  let n be Element of NAT;
  let P, Q be Subset of TOP-REAL n;
  func HausDist (P, Q) -> Real means
  :Def3:
  ex P9, Q9 being Subset of
  TopSpaceMetr Euclid n st P = P9 & Q = Q9 & it = HausDist (P9, Q9);
  existence
  proof
    the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
    then reconsider P9 = P, Q9 = Q as Subset of TopSpaceMetr Euclid n;
    take HausDist (P9, Q9), P9, Q9;
    thus thesis;
  end;
  uniqueness;
  commutativity;
end;

reserve n for Element of NAT;

theorem
  for P, Q being non empty Subset of TOP-REAL n st P is compact & Q is
  compact holds HausDist (P, Q) >= 0
proof
  let P, Q be non empty Subset of TOP-REAL n;
A1: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
  then reconsider P1 = P, Q1 = Q as non empty Subset of TopSpaceMetr Euclid n;
  assume P is compact & Q is compact;
  then P1 is compact & Q1 is compact by A1,COMPTS_1:23;
  then HausDist (P1, Q1) >= 0 by Th35;
  hence thesis by Def3;
end;

theorem
  for P being non empty Subset of TOP-REAL n holds HausDist (P, P) = 0
proof
  let P be non empty Subset of TOP-REAL n;
  the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
  then reconsider P1 = P as non empty Subset of TopSpaceMetr Euclid n;
  HausDist (P1, P1) = 0 by Th29;
  hence thesis by Def3;
end;

theorem
  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
proof
  let P, Q be non empty Subset of TOP-REAL n;
  assume that
A1: P is compact & Q is compact and
A2: HausDist (P, Q) = 0;
A3: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
  then reconsider P1 = P, Q1 = Q as non empty Subset of TopSpaceMetr Euclid n;
A4: HausDist (P1, Q1) = 0 by A2,Def3;
  P1 is compact & Q1 is compact by A1,A3,COMPTS_1:23;
  hence thesis by A4,Th37;
end;

theorem
  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)
proof
  let P, Q, R be non empty Subset of TOP-REAL n;
  assume that
A1: P is compact & Q is compact and
A2: R is compact;
A3: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
  then reconsider
  P1 = P, Q1 = Q, R1 = R as non empty Subset of TopSpaceMetr Euclid
  n;
A4: R1 is compact by A2,A3,COMPTS_1:23;
A5: HausDist (Q1, R1) = HausDist (Q, R) by Def3;
A6: HausDist (P1, R1) = HausDist (P, R) & HausDist (P1, Q1) = HausDist (P, Q
  ) by Def3;
  P1 is compact & Q1 is compact by A1,A3,COMPTS_1:23;
  hence thesis by A4,A6,A5,Th38;
end;