:: 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);