:: On the {H}ausdorff Distance Between Compact Subsets
:: by Adam Grabowski
::
:: Received January 27, 2003
:: Copyright (c) 2003-2026 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;
definitions XBOOLE_0, TARSKI, XXREAL_2;
equalities XBOOLE_0, STRUCT_0;
expansions 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, 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 st x >= 0 & max (x,y) = 0 holds x = 0
proof
let x, y be Real;
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 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;
assume y in (dist x) .: P;
then consider z being object 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 st p in X holds p >= 0 by Th4;
for q being Real st for p being Real 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 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;
assume r > 0;
then Ball (p, r) meets A by A1,GOBOARD6:92;
then consider x being object 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 st r > 0 ex q being Point of M st q in A &
dist (p, q) < r;
for r being Real st r > 0 holds Ball (p, r) meets A
proof
let r be Real;
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 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;
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 st p in X holds p >= r
proof
let p be Real;
assume p in X;
then consider y being object 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 st p in X holds p >= 0
proof
let p be Real;
assume p in X;
then consider y being object 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 st r > 0 ex p being Point of M st p in P &
dist (x, p) < r;
A12: for q being Real st for p being Real st p in X holds p >=
q holds 0 >= q
proof
let q be Real;
assume
A13: for z being Real 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 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 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 ExtReal;
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, 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, 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 st p in X holds p >= r
proof
let p be Real;
assume p in X;
then consider y being object 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 object 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;
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 object 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;
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 ExtReal;
assume p in X;
then consider z being object 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 ExtReal;
assume p in X;
then consider z being object 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 object such that
A1: x in P by XBOOLE_0:def 1;
thus (dist_min P) .: P c= { 0 }
proof
let y be object;
assume y in (dist_min P) .: P;
then
ex x being object 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 object;
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 st w in DPR holds w <= HausDist (P, Q) +
HausDist (Q, R)
proof
let w be Real;
assume w in DPR;
then consider y being object 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 st w in DPR holds w <= HausDist (P, Q) +
HausDist (Q, R)
proof
let w be Real;
assume w in DPR;
then consider y being object 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 object;
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 object;
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;