# Hausdorff distance #

The Hausdorff distance on subsets of a metric (or emetric) space.

Given two subsets s and t of a metric space, their Hausdorff distance is the smallest d such that any point s is within d of a point in t, and conversely. This quantity is often infinite (think of s bounded and t unbounded), and therefore better expressed in the setting of emetric spaces.

## Main definitions #

This files introduces:

• EMetric.infEdist x s, the infimum edistance of a point x to a set s in an emetric space
• EMetric.hausdorffEdist s t, the Hausdorff edistance of two sets in an emetric space
• Versions of these notions on metric spaces, called respectively Metric.infDist and Metric.hausdorffDist

## Main results #

• infEdist_closure: the edistance to a set and its closure coincide

• EMetric.mem_closure_iff_infEdist_zero: a point x belongs to the closure of s iff infEdist x s = 0

• IsCompact.exists_infEdist_eq_edist: if s is compact and non-empty, there exists a point y which attains this edistance

• IsOpen.exists_iUnion_isClosed: every open set U can be written as the increasing union of countably many closed subsets of U

• hausdorffEdist_closure: replacing a set by its closure does not change the Hausdorff edistance

• hausdorffEdist_zero_iff_closure_eq_closure: two sets have Hausdorff edistance zero iff their closures coincide

• the Hausdorff edistance is symmetric and satisfies the triangle inequality

• in particular, closed sets in an emetric space are an emetric space (this is shown in EMetricSpace.closeds.emetricspace)

• versions of these notions on metric spaces

• hausdorffEdist_ne_top_of_nonempty_of_bounded: if two sets in a metric space are nonempty and bounded in a metric space, they are at finite Hausdorff edistance.

## Tags #

metric space, Hausdorff distance

### Distance of a point to a set as a function into ℝ≥0∞. #

def EMetric.infEdist {α : Type u} (x : α) (s : Set α) :

The minimal edistance of a point to a set

Equations
Instances For
@[simp]
theorem EMetric.infEdist_empty {α : Type u} {x : α} :
theorem EMetric.le_infEdist {α : Type u} {x : α} {s : Set α} {d : ENNReal} :
d ys, d edist x y
@[simp]
theorem EMetric.infEdist_union {α : Type u} {x : α} {s : Set α} {t : Set α} :

The edist to a union is the minimum of the edists

@[simp]
theorem EMetric.infEdist_iUnion {ι : Sort u_1} {α : Type u} (f : ιSet α) (x : α) :
EMetric.infEdist x (⋃ (i : ι), f i) = ⨅ (i : ι), EMetric.infEdist x (f i)
theorem EMetric.infEdist_biUnion {α : Type u} {ι : Type u_2} (f : ιSet α) (I : Set ι) (x : α) :
EMetric.infEdist x (⋃ iI, f i) = iI, EMetric.infEdist x (f i)
@[simp]
theorem EMetric.infEdist_singleton {α : Type u} {x : α} {y : α} :

The edist to a singleton is the edistance to the single point of this singleton

theorem EMetric.infEdist_le_edist_of_mem {α : Type u} {x : α} {y : α} {s : Set α} (h : y s) :
edist x y

The edist to a set is bounded above by the edist to any of its points

theorem EMetric.infEdist_zero_of_mem {α : Type u} {x : α} {s : Set α} (h : x s) :
= 0

If a point x belongs to s, then its edist to s vanishes

theorem EMetric.infEdist_anti {α : Type u} {x : α} {s : Set α} {t : Set α} (h : s t) :

The edist is antitone with respect to inclusion.

theorem EMetric.infEdist_lt_iff {α : Type u} {x : α} {s : Set α} {r : ENNReal} :
< r ys, edist x y < r

The edist to a set is < r iff there exists a point in the set at edistance < r

theorem EMetric.infEdist_le_infEdist_add_edist {α : Type u} {x : α} {y : α} {s : Set α} :
+ edist x y

The edist of x to s is bounded by the sum of the edist of y to s and the edist from x to y

theorem EMetric.infEdist_le_edist_add_infEdist {α : Type u} {x : α} {y : α} {s : Set α} :
edist x y +
theorem EMetric.edist_le_infEdist_add_ediam {α : Type u} {x : α} {y : α} {s : Set α} (hy : y s) :
edist x y
theorem EMetric.continuous_infEdist {α : Type u} {s : Set α} :
Continuous fun (x : α) =>

The edist to a set depends continuously on the point

theorem EMetric.infEdist_closure {α : Type u} {x : α} {s : Set α} :
=

The edist to a set and to its closure coincide

theorem EMetric.mem_closure_iff_infEdist_zero {α : Type u} {x : α} {s : Set α} :
x = 0

A point belongs to the closure of s iff its infimum edistance to this set vanishes

theorem EMetric.mem_iff_infEdist_zero_of_closed {α : Type u} {x : α} {s : Set α} (h : ) :
x s = 0

Given a closed set s, a point belongs to s iff its infimum edistance to this set vanishes

theorem EMetric.infEdist_pos_iff_not_mem_closure {α : Type u} {x : α} {E : Set α} :
0 < x

The infimum edistance of a point to a set is positive if and only if the point is not in the closure of the set.

theorem EMetric.infEdist_closure_pos_iff_not_mem_closure {α : Type u} {x : α} {E : Set α} :
0 < x
theorem EMetric.exists_real_pos_lt_infEdist_of_not_mem_closure {α : Type u} {x : α} {E : Set α} (h : x) :
∃ (ε : ), 0 < ε
theorem EMetric.disjoint_closedBall_of_lt_infEdist {α : Type u} {x : α} {s : Set α} {r : ENNReal} (h : r < ) :
theorem EMetric.infEdist_image {α : Type u} {β : Type v} {x : α} {t : Set α} {Φ : αβ} (hΦ : ) :
EMetric.infEdist (Φ x) (Φ '' t) =

The infimum edistance is invariant under isometries

@[simp]
theorem EMetric.infEdist_vadd {α : Type u} {M : Type u_2} [VAdd M α] [] (c : M) (x : α) (s : Set α) :
@[simp]
theorem EMetric.infEdist_smul {α : Type u} {M : Type u_2} [SMul M α] [] (c : M) (x : α) (s : Set α) :
EMetric.infEdist (c x) (c s) =
theorem IsOpen.exists_iUnion_isClosed {α : Type u} {U : Set α} (hU : ) :
∃ (F : Set α), (∀ (n : ), IsClosed (F n)) (∀ (n : ), F n U) ⋃ (n : ), F n = U
theorem IsCompact.exists_infEdist_eq_edist {α : Type u} {s : Set α} (hs : ) (hne : s.Nonempty) (x : α) :
ys, = edist x y
theorem EMetric.exists_pos_forall_lt_edist {α : Type u} {s : Set α} {t : Set α} (hs : ) (ht : ) (hst : Disjoint s t) :
∃ (r : NNReal), 0 < r xs, yt, r < edist x y

### The Hausdorff distance as a function into ℝ≥0∞. #

@[irreducible]
def EMetric.hausdorffEdist {α : Type u_2} (s : Set α) (t : Set α) :

The Hausdorff edistance between two sets is the smallest r such that each set is contained in the r-neighborhood of the other one

Equations
Instances For
theorem EMetric.hausdorffEdist_def {α : Type u_2} (s : Set α) (t : Set α) :
= (⨆ xs, ) yt,
@[simp]
theorem EMetric.hausdorffEdist_self {α : Type u} {s : Set α} :

The Hausdorff edistance of a set to itself vanishes.

theorem EMetric.hausdorffEdist_comm {α : Type u} {s : Set α} {t : Set α} :

The Haudorff edistances of s to t and of t to s coincide.

theorem EMetric.hausdorffEdist_le_of_infEdist {α : Type u} {s : Set α} {t : Set α} {r : ENNReal} (H1 : xs, r) (H2 : xt, r) :

Bounding the Hausdorff edistance by bounding the edistance of any point in each set to the other set

theorem EMetric.hausdorffEdist_le_of_mem_edist {α : Type u} {s : Set α} {t : Set α} {r : ENNReal} (H1 : xs, yt, edist x y r) (H2 : xt, ys, edist x y r) :

Bounding the Hausdorff edistance by exhibiting, for any point in each set, another point in the other set at controlled distance

theorem EMetric.infEdist_le_hausdorffEdist_of_mem {α : Type u} {x : α} {s : Set α} {t : Set α} (h : x s) :

The distance to a set is controlled by the Hausdorff distance.

theorem EMetric.exists_edist_lt_of_hausdorffEdist_lt {α : Type u} {x : α} {s : Set α} {t : Set α} {r : ENNReal} (h : x s) (H : ) :
yt, edist x y < r

If the Hausdorff distance is < r, then any point in one of the sets has a corresponding point at distance < r in the other set.

theorem EMetric.infEdist_le_infEdist_add_hausdorffEdist {α : Type u} {x : α} {s : Set α} {t : Set α} :

The distance from x to s or t is controlled in terms of the Hausdorff distance between s and t.

theorem EMetric.hausdorffEdist_image {α : Type u} {β : Type v} {s : Set α} {t : Set α} {Φ : αβ} (h : ) :
EMetric.hausdorffEdist (Φ '' s) (Φ '' t) =

The Hausdorff edistance is invariant under isometries.

theorem EMetric.hausdorffEdist_le_ediam {α : Type u} {s : Set α} {t : Set α} (hs : s.Nonempty) (ht : t.Nonempty) :

The Hausdorff distance is controlled by the diameter of the union.

theorem EMetric.hausdorffEdist_triangle {α : Type u} {s : Set α} {t : Set α} {u : Set α} :

The Hausdorff distance satisfies the triangle inequality.

theorem EMetric.hausdorffEdist_zero_iff_closure_eq_closure {α : Type u} {s : Set α} {t : Set α} :
=

Two sets are at zero Hausdorff edistance if and only if they have the same closure.

@[simp]
theorem EMetric.hausdorffEdist_self_closure {α : Type u} {s : Set α} :
= 0

The Hausdorff edistance between a set and its closure vanishes.

@[simp]
theorem EMetric.hausdorffEdist_closure₁ {α : Type u} {s : Set α} {t : Set α} :

Replacing a set by its closure does not change the Hausdorff edistance.

@[simp]
theorem EMetric.hausdorffEdist_closure₂ {α : Type u} {s : Set α} {t : Set α} :

Replacing a set by its closure does not change the Hausdorff edistance.

theorem EMetric.hausdorffEdist_closure {α : Type u} {s : Set α} {t : Set α} :

The Hausdorff edistance between sets or their closures is the same.

theorem EMetric.hausdorffEdist_zero_iff_eq_of_closed {α : Type u} {s : Set α} {t : Set α} (hs : ) (ht : ) :
s = t

Two closed sets are at zero Hausdorff edistance if and only if they coincide.

theorem EMetric.hausdorffEdist_empty {α : Type u} {s : Set α} (ne : s.Nonempty) :

The Haudorff edistance to the empty set is infinite.

theorem EMetric.nonempty_of_hausdorffEdist_ne_top {α : Type u} {s : Set α} {t : Set α} (hs : s.Nonempty) (fin : ) :
t.Nonempty

If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty.

theorem EMetric.empty_or_nonempty_of_hausdorffEdist_ne_top {α : Type u} {s : Set α} {t : Set α} (fin : ) :
s = t = s.Nonempty t.Nonempty

Now, we turn to the same notions in metric spaces. To avoid the difficulties related to sInf and sSup on ℝ (which is only conditionally complete), we use the notions in ℝ≥0∞ formulated in terms of the edistance, and coerce them to ℝ. Then their properties follow readily from the corresponding properties in ℝ≥0∞, modulo some tedious rewriting of inequalities from one to the other.

### Distance of a point to a set as a function into ℝ. #

def Metric.infDist {α : Type u} (x : α) (s : Set α) :

The minimal distance of a point to a set

Equations
Instances For
theorem Metric.infDist_eq_iInf {α : Type u} {s : Set α} {x : α} :
= ⨅ (y : s), dist x y
theorem Metric.infDist_nonneg {α : Type u} {s : Set α} {x : α} :
0

The minimal distance is always nonnegative

@[simp]
theorem Metric.infDist_empty {α : Type u} {x : α} :
= 0

The minimal distance to the empty set is 0 (if you want to have the more reasonable value ∞ instead, use EMetric.infEdist, which takes values in ℝ≥0∞)

theorem Metric.infEdist_ne_top {α : Type u} {s : Set α} {x : α} (h : s.Nonempty) :

In a metric space, the minimal edistance to a nonempty set is finite.

theorem Metric.infEdist_eq_top_iff {α : Type u} {s : Set α} {x : α} :
s =
theorem Metric.infDist_zero_of_mem {α : Type u} {s : Set α} {x : α} (h : x s) :
= 0

The minimal distance of a point to a set containing it vanishes.

@[simp]
theorem Metric.infDist_singleton {α : Type u} {x : α} {y : α} :

The minimal distance to a singleton is the distance to the unique point in this singleton.

theorem Metric.infDist_le_dist_of_mem {α : Type u} {s : Set α} {x : α} {y : α} (h : y s) :
dist x y

The minimal distance to a set is bounded by the distance to any point in this set.

theorem Metric.infDist_le_infDist_of_subset {α : Type u} {s : Set α} {t : Set α} {x : α} (h : s t) (hs : s.Nonempty) :

The minimal distance is monotone with respect to inclusion.

theorem Metric.infDist_lt_iff {α : Type u} {s : Set α} {x : α} {r : } (hs : s.Nonempty) :
< r ys, dist x y < r

The minimal distance to a set s is < r iff there exists a point in s at distance < r.

theorem Metric.infDist_le_infDist_add_dist {α : Type u} {s : Set α} {x : α} {y : α} :
+ dist x y

The minimal distance from x to s is bounded by the distance from y to s, modulo the distance between x and y.

theorem Metric.not_mem_of_dist_lt_infDist {α : Type u} {s : Set α} {x : α} {y : α} (h : dist x y < ) :
ys
theorem Metric.disjoint_ball_infDist {α : Type u} {s : Set α} {x : α} :
theorem Metric.ball_infDist_subset_compl {α : Type u} {s : Set α} {x : α} :
theorem Metric.ball_infDist_compl_subset {α : Type u} {s : Set α} {x : α} :
theorem Metric.disjoint_closedBall_of_lt_infDist {α : Type u} {s : Set α} {x : α} {r : } (h : r < ) :
theorem Metric.dist_le_infDist_add_diam {α : Type u} {s : Set α} {x : α} {y : α} (hs : ) (hy : y s) :
dist x y
theorem Metric.lipschitz_infDist_pt {α : Type u} (s : Set α) :
LipschitzWith 1 fun (x : α) =>

The minimal distance to a set is Lipschitz in point with constant 1

theorem Metric.uniformContinuous_infDist_pt {α : Type u} (s : Set α) :
UniformContinuous fun (x : α) =>

The minimal distance to a set is uniformly continuous in point

theorem Metric.continuous_infDist_pt {α : Type u} (s : Set α) :
Continuous fun (x : α) =>

The minimal distance to a set is continuous in point

theorem Metric.infDist_closure {α : Type u} {s : Set α} {x : α} :
=

The minimal distances to a set and its closure coincide.

theorem Metric.infDist_zero_of_mem_closure {α : Type u} {s : Set α} {x : α} (hx : x ) :
= 0

If a point belongs to the closure of s, then its infimum distance to s equals zero. The converse is true provided that s is nonempty, see Metric.mem_closure_iff_infDist_zero.

theorem Metric.mem_closure_iff_infDist_zero {α : Type u} {s : Set α} {x : α} (h : s.Nonempty) :
x = 0

A point belongs to the closure of s iff its infimum distance to this set vanishes.

theorem IsClosed.mem_iff_infDist_zero {α : Type u} {s : Set α} {x : α} (h : ) (hs : s.Nonempty) :
x s = 0

Given a closed set s, a point belongs to s iff its infimum distance to this set vanishes

theorem IsClosed.not_mem_iff_infDist_pos {α : Type u} {s : Set α} {x : α} (h : ) (hs : s.Nonempty) :
xs 0 <

Given a closed set s, a point belongs to s iff its infimum distance to this set vanishes.

theorem Metric.continuousAt_inv_infDist_pt {α : Type u} {s : Set α} {x : α} (h : x) :
ContinuousAt (fun (x : α) => (Metric.infDist x s)⁻¹) x
theorem Metric.infDist_image {α : Type u} {β : Type v} {t : Set α} {x : α} {Φ : αβ} (hΦ : ) :
Metric.infDist (Φ x) (Φ '' t) =

The infimum distance is invariant under isometries.

theorem Metric.infDist_inter_closedBall_of_mem {α : Type u} {s : Set α} {x : α} {y : α} (h : y s) :
theorem IsCompact.exists_infDist_eq_dist {α : Type u} {s : Set α} (h : ) (hne : s.Nonempty) (x : α) :
ys, = dist x y
theorem IsClosed.exists_infDist_eq_dist {α : Type u} {s : Set α} [] (h : ) (hne : s.Nonempty) (x : α) :
ys, = dist x y
theorem Metric.exists_mem_closure_infDist_eq_dist {α : Type u} {s : Set α} [] (hne : s.Nonempty) (x : α) :
y, = dist x y

### Distance of a point to a set as a function into ℝ≥0. #

def Metric.infNndist {α : Type u} (x : α) (s : Set α) :

The minimal distance of a point to a set as a ℝ≥0

Equations
Instances For
@[simp]
theorem Metric.coe_infNndist {α : Type u} {s : Set α} {x : α} :
theorem Metric.lipschitz_infNndist_pt {α : Type u} (s : Set α) :
LipschitzWith 1 fun (x : α) =>

The minimal distance to a set (as ℝ≥0) is Lipschitz in point with constant 1

theorem Metric.uniformContinuous_infNndist_pt {α : Type u} (s : Set α) :
UniformContinuous fun (x : α) =>

The minimal distance to a set (as ℝ≥0) is uniformly continuous in point

theorem Metric.continuous_infNndist_pt {α : Type u} (s : Set α) :
Continuous fun (x : α) =>

The minimal distance to a set (as ℝ≥0) is continuous in point

### The Hausdorff distance as a function into ℝ. #

def Metric.hausdorffDist {α : Type u} (s : Set α) (t : Set α) :

The Hausdorff distance between two sets is the smallest nonnegative r such that each set is included in the r-neighborhood of the other. If there is no such r, it is defined to be 0, arbitrarily.

Equations
• = .toReal
Instances For
theorem Metric.hausdorffDist_nonneg {α : Type u} {s : Set α} {t : Set α} :

The Hausdorff distance is nonnegative.

theorem Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded {α : Type u} {s : Set α} {t : Set α} (hs : s.Nonempty) (ht : t.Nonempty) (bs : ) (bt : ) :

If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff edistance.

@[simp]
theorem Metric.hausdorffDist_self_zero {α : Type u} {s : Set α} :

The Hausdorff distance between a set and itself is zero.

theorem Metric.hausdorffDist_comm {α : Type u} {s : Set α} {t : Set α} :

The Hausdorff distances from s to t and from t to s coincide.

@[simp]
theorem Metric.hausdorffDist_empty {α : Type u} {s : Set α} :

The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable value ∞ instead, use EMetric.hausdorffEdist, which takes values in ℝ≥0∞).

@[simp]
theorem Metric.hausdorffDist_empty' {α : Type u} {s : Set α} :

The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable value ∞ instead, use EMetric.hausdorffEdist, which takes values in ℝ≥0∞).

theorem Metric.hausdorffDist_le_of_infDist {α : Type u} {s : Set α} {t : Set α} {r : } (hr : 0 r) (H1 : xs, r) (H2 : xt, r) :

Bounding the Hausdorff distance by bounding the distance of any point in each set to the other set

theorem Metric.hausdorffDist_le_of_mem_dist {α : Type u} {s : Set α} {t : Set α} {r : } (hr : 0 r) (H1 : xs, yt, dist x y r) (H2 : xt, ys, dist x y r) :

Bounding the Hausdorff distance by exhibiting, for any point in each set, another point in the other set at controlled distance

theorem Metric.hausdorffDist_le_diam {α : Type u} {s : Set α} {t : Set α} (hs : s.Nonempty) (bs : ) (ht : t.Nonempty) (bt : ) :

The Hausdorff distance is controlled by the diameter of the union.

theorem Metric.infDist_le_hausdorffDist_of_mem {α : Type u} {s : Set α} {t : Set α} {x : α} (hx : x s) (fin : ) :

The distance to a set is controlled by the Hausdorff distance.

theorem Metric.exists_dist_lt_of_hausdorffDist_lt {α : Type u} {s : Set α} {t : Set α} {x : α} {r : } (h : x s) (H : ) (fin : ) :
yt, dist x y < r

If the Hausdorff distance is < r, any point in one of the sets is at distance < r of a point in the other set.

theorem Metric.exists_dist_lt_of_hausdorffDist_lt' {α : Type u} {s : Set α} {t : Set α} {y : α} {r : } (h : y t) (H : ) (fin : ) :
xs, dist x y < r

If the Hausdorff distance is < r, any point in one of the sets is at distance < r of a point in the other set.

theorem Metric.infDist_le_infDist_add_hausdorffDist {α : Type u} {s : Set α} {t : Set α} {x : α} (fin : ) :

The infimum distance to s and t are the same, up to the Hausdorff distance between s and t

theorem Metric.hausdorffDist_image {α : Type u} {β : Type v} {s : Set α} {t : Set α} {Φ : αβ} (h : ) :
Metric.hausdorffDist (Φ '' s) (Φ '' t) =

The Hausdorff distance is invariant under isometries.

theorem Metric.hausdorffDist_triangle {α : Type u} {s : Set α} {t : Set α} {u : Set α} (fin : ) :

The Hausdorff distance satisfies the triangle inequality.

theorem Metric.hausdorffDist_triangle' {α : Type u} {s : Set α} {t : Set α} {u : Set α} (fin : ) :

The Hausdorff distance satisfies the triangle inequality.

@[simp]
theorem Metric.hausdorffDist_self_closure {α : Type u} {s : Set α} :
= 0

The Hausdorff distance between a set and its closure vanishes.

@[simp]
theorem Metric.hausdorffDist_closure₁ {α : Type u} {s : Set α} {t : Set α} :

Replacing a set by its closure does not change the Hausdorff distance.

@[simp]
theorem Metric.hausdorffDist_closure₂ {α : Type u} {s : Set α} {t : Set α} :

Replacing a set by its closure does not change the Hausdorff distance.

theorem Metric.hausdorffDist_closure {α : Type u} {s : Set α} {t : Set α} :
=

The Hausdorff distances between two sets and their closures coincide.

theorem Metric.hausdorffDist_zero_iff_closure_eq_closure {α : Type u} {s : Set α} {t : Set α} (fin : ) :
=

Two sets are at zero Hausdorff distance if and only if they have the same closures.

theorem IsClosed.hausdorffDist_zero_iff_eq {α : Type u} {s : Set α} {t : Set α} (hs : ) (ht : ) (fin : ) :
s = t

Two closed sets are at zero Hausdorff distance if and only if they coincide.