# mathlibdocumentation

topology.metric_space.hausdorff_distance

# 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:

• inf_edist x s, the infimum edistance of a point x to a set s in an emetric space
• Hausdorff_edist s t, the Hausdorff edistance of two sets in an emetric space
• Versions of these notions on metric spaces, called respectively inf_dist and Hausdorff_dist.

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

def emetric.inf_edist {α : Type u} (x : α) (s : set α) :

The minimal edistance of a point to a set

Equations
• = ⨅ (y : α) (H : y s), y
@[simp]
theorem emetric.inf_edist_empty {α : Type u} {x : α} :
theorem emetric.le_inf_edist {α : Type u} {x : α} {s : set α} {d : ℝ≥0∞} :
d ∀ (y : α), y sd y
@[simp]
theorem emetric.inf_edist_union {α : Type u} {x : α} {s t : set α} :
(s t) =

The edist to a union is the minimum of the edists

@[simp]
theorem emetric.inf_edist_singleton {α : Type u} {x y : α} :
{y} = y

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

theorem emetric.inf_edist_le_edist_of_mem {α : Type u} {x y : α} {s : set α} (h : y s) :
y

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

theorem emetric.inf_edist_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.inf_edist_le_inf_edist_of_subset {α : Type u} {x : α} {s t : set α} (h : s t) :

The edist is monotonous with respect to inclusion

theorem emetric.exists_edist_lt_of_inf_edist_lt {α : Type u} {x : α} {s : set α} {r : ℝ≥0∞} (h : < r) :
∃ (y : α) (H : y s), y < r

If the edist to a set is < r, there exists a point in the set at edistance < r

theorem emetric.inf_edist_le_inf_edist_add_edist {α : Type u} {x y : α} {s : set α} :
+ 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.continuous_inf_edist {α : Type u} {s : set α} :
continuous (λ (x : α),

The edist to a set depends continuously on the point

theorem emetric.inf_edist_closure {α : Type u} {x : α} {s : set α} :
(closure s) =

The edist to a set and to its closure coincide

theorem emetric.mem_closure_iff_inf_edist_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_inf_edist_zero_of_closed {α : Type u} {x : α} {s : set α} (h : is_closed s) :
x s = 0

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

theorem emetric.disjoint_closed_ball_of_lt_inf_edist {α : Type u} {x : α} {s : set α} {r : ℝ≥0∞} (h : r < ) :
s
theorem emetric.inf_edist_image {α : Type u} {β : Type v} {x : α} {t : set α} {Φ : α → β} (hΦ : isometry Φ) :
emetric.inf_edist (Φ x) '' t) =

The infimum edistance is invariant under isometries

theorem is_open.exists_Union_is_closed {α : Type u} {U : set α} (hU : is_open U) :
∃ (F : set α), (∀ (n : ), is_closed (F n)) (∀ (n : ), F n U) (⋃ (n : ), F n) = U

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

def emetric.Hausdorff_edist {α : Type u} (s 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
• = (⨆ (x : α) (H : x s), ⨆ (y : α) (H : y t),
theorem emetric.Hausdorff_edist_def {α : Type u} (s t : set α) :
= (⨆ (x : α) (H : x s), ⨆ (y : α) (H : y t),
@[simp]
theorem emetric.Hausdorff_edist_self {α : Type u} {s : set α} :

The Hausdorff edistance of a set to itself vanishes

theorem emetric.Hausdorff_edist_comm {α : Type u} {s t : set α} :

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

theorem emetric.Hausdorff_edist_le_of_inf_edist {α : Type u} {s t : set α} {r : ℝ≥0∞} (H1 : ∀ (x : α), x s r) (H2 : ∀ (x : α), x t r) :

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

theorem emetric.Hausdorff_edist_le_of_mem_edist {α : Type u} {s t : set α} {r : ℝ≥0∞} (H1 : ∀ (x : α), x s(∃ (y : α) (H : y t), y r)) (H2 : ∀ (x : α), x t(∃ (y : α) (H : y s), 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.inf_edist_le_Hausdorff_edist_of_mem {α : Type u} {x : α} {s t : set α} (h : x s) :

The distance to a set is controlled by the Hausdorff distance

theorem emetric.exists_edist_lt_of_Hausdorff_edist_lt {α : Type u} {x : α} {s t : set α} {r : ℝ≥0∞} (h : x s) (H : < r) :
∃ (y : α) (H : y t), 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.inf_edist_le_inf_edist_add_Hausdorff_edist {α : Type u} {x : α} {s t : set α} :

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

theorem emetric.Hausdorff_edist_image {α : Type u} {β : Type v} {s t : set α} {Φ : α → β} (h : isometry Φ) :
'' t) =

The Hausdorff edistance is invariant under eisometries

theorem emetric.Hausdorff_edist_le_ediam {α : Type u} {s t : set α} (hs : s.nonempty) (ht : t.nonempty) :

The Hausdorff distance is controlled by the diameter of the union

theorem emetric.Hausdorff_edist_triangle {α : Type u} {s t u : set α} :

The Hausdorff distance satisfies the triangular inequality

theorem emetric.Hausdorff_edist_zero_iff_closure_eq_closure {α : Type u} {s t : set α} :
=

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

@[simp]
theorem emetric.Hausdorff_edist_self_closure {α : Type u} {s : set α} :
= 0

The Hausdorff edistance between a set and its closure vanishes

@[simp]
theorem emetric.Hausdorff_edist_closure₁ {α : Type u} {s t : set α} :

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

@[simp]
theorem emetric.Hausdorff_edist_closure₂ {α : Type u} {s t : set α} :

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

@[simp]
theorem emetric.Hausdorff_edist_closure {α : Type u} {s t : set α} :

The Hausdorff edistance between sets or their closures is the same

theorem emetric.Hausdorff_edist_zero_iff_eq_of_closed {α : Type u} {s t : set α} (hs : is_closed s) (ht : is_closed t) :
s = t

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

theorem emetric.Hausdorff_edist_empty {α : Type u} {s : set α} (ne : s.nonempty) :

The Haudorff edistance to the empty set is infinite

theorem emetric.nonempty_of_Hausdorff_edist_ne_top {α : Type u} {s t : set α} (hs : s.nonempty) (fin : ) :

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

theorem emetric.empty_or_nonempty_of_Hausdorff_edist_ne_top {α : Type u} {s t : set α} (fin : ) :
s = t =

Now, we turn to the same notions in metric spaces. To avoid the difficulties related to Inf and Sup 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.inf_dist {α : Type u} (x : α) (s : set α) :

The minimal distance of a point to a set

Equations
theorem metric.inf_dist_nonneg {α : Type u} {s : set α} {x : α} :
0

the minimal distance is always nonnegative

@[simp]
theorem metric.inf_dist_empty {α : Type u} {x : α} :

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

theorem metric.inf_edist_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.inf_dist_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.inf_dist_singleton {α : Type u} {x y : α} :
{y} = dist x y

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

theorem metric.inf_dist_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.inf_dist_le_inf_dist_of_subset {α : Type u} {s t : set α} {x : α} (h : s t) (hs : s.nonempty) :

The minimal distance is monotonous with respect to inclusion

theorem metric.exists_dist_lt_of_inf_dist_lt {α : Type u} {s : set α} {x : α} {r : } (h : < r) (hs : s.nonempty) :
∃ (y : α) (H : y s), dist x y < r

If the minimal distance to a set is <r, there exists a point in this set at distance <r

theorem metric.inf_dist_le_inf_dist_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.disjoint_closed_ball_of_lt_inf_dist {α : Type u} {s : set α} {x : α} {r : } (h : r < ) :
s
theorem metric.lipschitz_inf_dist_pt {α : Type u} (s : set α) :
(λ (x : α), s)

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

theorem metric.uniform_continuous_inf_dist_pt {α : Type u} (s : set α) :
uniform_continuous (λ (x : α), s)

The minimal distance to a set is uniformly continuous in point

theorem metric.continuous_inf_dist_pt {α : Type u} (s : set α) :
continuous (λ (x : α), s)

The minimal distance to a set is continuous in point

theorem metric.inf_dist_eq_closure {α : Type u} {s : set α} {x : α} :
(closure s) =

The minimal distance to a set and its closure coincide

theorem metric.mem_closure_iff_inf_dist_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 is_closed.mem_iff_inf_dist_zero {α : Type u} {s : set α} {x : α} (h : is_closed s) (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 is_closed.not_mem_iff_inf_dist_pos {α : Type u} {s : set α} {x : α} (h : is_closed s) (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 metric.inf_dist_image {α : Type u} {β : Type v} {t : set α} {x : α} {Φ : α → β} (hΦ : isometry Φ) :
metric.inf_dist (Φ x) '' t) =

The infimum distance is invariant under isometries

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

def metric.inf_nndist {α : Type u} (x : α) (s : set α) :

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

Equations
@[simp]
theorem metric.coe_inf_nndist {α : Type u} {s : set α} {x : α} :
s) =
theorem metric.lipschitz_inf_nndist_pt {α : Type u} (s : set α) :
(λ (x : α),

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

theorem metric.uniform_continuous_inf_nndist_pt {α : Type u} (s : set α) :
uniform_continuous (λ (x : α),

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

theorem metric.continuous_inf_nndist_pt {α : Type u} (s : set α) :
continuous (λ (x : α),

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

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

def metric.Hausdorff_dist {α : Type u} (s 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
theorem metric.Hausdorff_dist_nonneg {α : Type u} {s t : set α} :

The Hausdorff distance is nonnegative

theorem metric.Hausdorff_edist_ne_top_of_nonempty_of_bounded {α : Type u} {s t : set α} (hs : s.nonempty) (ht : t.nonempty) (bs : metric.bounded s) (bt : metric.bounded t) :

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

@[simp]
theorem metric.Hausdorff_dist_self_zero {α : Type u} {s : set α} :

The Hausdorff distance between a set and itself is zero

theorem metric.Hausdorff_dist_comm {α : Type u} {s t : set α} :

The Hausdorff distance from s to t and from t to s coincide

@[simp]
theorem metric.Hausdorff_dist_empty {α : Type u} {s : set α} :

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

@[simp]
theorem metric.Hausdorff_dist_empty' {α : Type u} {s : set α} :

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

theorem metric.Hausdorff_dist_le_of_inf_dist {α : Type u} {s t : set α} {r : } (hr : 0 r) (H1 : ∀ (x : α), x s r) (H2 : ∀ (x : α), x t r) :

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

theorem metric.Hausdorff_dist_le_of_mem_dist {α : Type u} {s t : set α} {r : } (hr : 0 r) (H1 : ∀ (x : α), x s(∃ (y : α) (H : y t), dist x y r)) (H2 : ∀ (x : α), x t(∃ (y : α) (H : y s), 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.Hausdorff_dist_le_diam {α : Type u} {s t : set α} (hs : s.nonempty) (bs : metric.bounded s) (ht : t.nonempty) (bt : metric.bounded t) :

The Hausdorff distance is controlled by the diameter of the union

theorem metric.inf_dist_le_Hausdorff_dist_of_mem {α : Type u} {s t : set α} {x : α} (hx : x s) (fin : ) :

The distance to a set is controlled by the Hausdorff distance

theorem metric.exists_dist_lt_of_Hausdorff_dist_lt {α : Type u} {s t : set α} {x : α} {r : } (h : x s) (H : < r) (fin : ) :
∃ (y : α) (H : y t), dist x y < r

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

theorem metric.exists_dist_lt_of_Hausdorff_dist_lt' {α : Type u} {s t : set α} {y : α} {r : } (h : y t) (H : < r) (fin : ) :
∃ (x : α) (H : x s), dist x y < r

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

theorem metric.inf_dist_le_inf_dist_add_Hausdorff_dist {α : Type u} {s 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.Hausdorff_dist_image {α : Type u} {β : Type v} {s t : set α} {Φ : α → β} (h : isometry Φ) :
metric.Hausdorff_dist '' s) '' t) =

The Hausdorff distance is invariant under isometries

theorem metric.Hausdorff_dist_triangle {α : Type u} {s t u : set α} (fin : ) :

The Hausdorff distance satisfies the triangular inequality

theorem metric.Hausdorff_dist_triangle' {α : Type u} {s t u : set α} (fin : ) :

The Hausdorff distance satisfies the triangular inequality

@[simp]
theorem metric.Hausdorff_dist_self_closure {α : Type u} {s : set α} :
= 0

The Hausdorff distance between a set and its closure vanish

@[simp]
theorem metric.Hausdorff_dist_closure₁ {α : Type u} {s t : set α} :

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

@[simp]
theorem metric.Hausdorff_dist_closure₂ {α : Type u} {s t : set α} :

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

@[simp]
theorem metric.Hausdorff_dist_closure {α : Type u} {s t : set α} :

The Hausdorff distance between two sets and their closures coincide

theorem metric.Hausdorff_dist_zero_iff_closure_eq_closure {α : Type u} {s t : set α} (fin : ) :
=

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

theorem is_closed.Hausdorff_dist_zero_iff_eq {α : Type u} {s t : set α} (hs : is_closed s) (ht : is_closed t) (fin : ) :
s = t

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