Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

## On the Hausdorff Distance Between Compact Subsets

University of Bialystok

### Summary.

In [2] the pseudo-metric ${\rm dist}^{\rm max}_{\rm min}$ on compact subsets $A$ and $B$ of a topological space generated from arbitrary metric space is defined. Using this notion we define the Hausdorff distance (see e.g. [6]) of $A$ and $B$ as a maximum of the two pseudo-distances: from $A$ to $B$ and from $B$ to $A$. We justify its distance properties. At the end we define some special notions which enable to apply the Hausdorff distance operator ${\rm HausDist"}$ to the subsets of the Euclidean topological space~$\calE^n_T.$

This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102 and TYPES grant IST-1999-29001.

#### MML Identifier: HAUSDORF

The terminology and notation used in this paper have been introduced in the following articles [16] [19] [1] [17] [11] [18] [20] [4] [15] [7] [10] [9] [12] [3] [8] [5] [2] [14] [13]

#### Contents (PDF format)

1. Preliminaries
2. The Hausdorff Distance

#### Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Jozef Bialas and Yatsuka Nakamura. The theorem of Weierstrass. Journal of Formalized Mathematics, 7, 1995.
[3] Leszek Borys. Paracompact and metrizable spaces. Journal of Formalized Mathematics, 3, 1991.
[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski and Piotr Rudnicki. Bounding boxes for compact sets in $\calE^2$. Journal of Formalized Mathematics, 9, 1997.
[7] Agata Darmochwal. Compact spaces. Journal of Formalized Mathematics, 1, 1989.
[8] Agata Darmochwal. The Euclidean space. Journal of Formalized Mathematics, 3, 1991.
[9] Agata Darmochwal and Yatsuka Nakamura. Metric spaces as topological spaces --- fundamental concepts. Journal of Formalized Mathematics, 3, 1991.
[10] Alicia de la Cruz. Totally bounded metric spaces. Journal of Formalized Mathematics, 3, 1991.
[11] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.
[12] Stanislawa Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Journal of Formalized Mathematics, 2, 1990.
[13] Jaroslaw Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Journal of Formalized Mathematics, 1, 1989.
[14] Beata Padlewska. Locally connected spaces. Journal of Formalized Mathematics, 2, 1990.
[15] Beata Padlewska and Agata Darmochwal. Topological spaces and continuous functions. Journal of Formalized Mathematics, 1, 1989.
[16] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[17] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[18] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.
[19] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[20] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.