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} [PseudoEMetricSpace α] (x : α) (s : Set α) : ENNReal

The minimal edistance of a point to a set

Equations

• EMetric.infEdist x s = ⨅ y ∈ s, edist x y

@[simp]

theorem EMetric.infEdist_empty {α : Type u} [PseudoEMetricSpace α] {x : α} : EMetric.infEdist x ∅ = ⊤

theorem EMetric.le_infEdist {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} {d : ENNReal} : d ≤ EMetric.infEdist x s ↔ ∀ y ∈ s, d ≤ edist x y

@[simp]

theorem EMetric.infEdist_union {α : Type u} [PseudoEMetricSpace α] {x : α} {s t : Set α} : EMetric.infEdist x (s ∪ t) = EMetric.infEdist x s ⊓ EMetric.infEdist x t

The edist to a union is the minimum of the edists

@[simp]

theorem EMetric.infEdist_iUnion {ι : Sort u_1} {α : Type u} [PseudoEMetricSpace α] (f : ι → Set α) (x : α) : EMetric.infEdist x (⋃ (i : ι), f i) = ⨅ (i : ι), EMetric.infEdist x (f i)

theorem EMetric.infEdist_biUnion {α : Type u} [PseudoEMetricSpace α] {ι : Type u_2} (f : ι → Set α) (I : Set ι) (x : α) : EMetric.infEdist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, EMetric.infEdist x (f i)

@[simp]

theorem EMetric.infEdist_singleton {α : Type u} [PseudoEMetricSpace α] {x y : α} : EMetric.infEdist x {y} = edist 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} [PseudoEMetricSpace α] {x y : α} {s : Set α} (h : y ∈ s) : EMetric.infEdist x 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} [PseudoEMetricSpace α] {x : α} {s : Set α} (h : x ∈ s) : EMetric.infEdist x s = 0

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

theorem EMetric.infEdist_anti {α : Type u} [PseudoEMetricSpace α] {x : α} {s t : Set α} (h : s ⊆ t) : EMetric.infEdist x t ≤ EMetric.infEdist x s

The edist is antitone with respect to inclusion.

theorem EMetric.infEdist_lt_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} {r : ENNReal} : EMetric.infEdist x s < r ↔ ∃ y ∈ s, 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} [PseudoEMetricSpace α] {x y : α} {s : Set α} : EMetric.infEdist x s ≤ EMetric.infEdist y s + 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} [PseudoEMetricSpace α] {x y : α} {s : Set α} : EMetric.infEdist x s ≤ edist x y + EMetric.infEdist y s

theorem EMetric.edist_le_infEdist_add_ediam {α : Type u} [PseudoEMetricSpace α] {x y : α} {s : Set α} (hy : y ∈ s) : edist x y ≤ EMetric.infEdist x s + EMetric.diam s

theorem EMetric.continuous_infEdist {α : Type u} [PseudoEMetricSpace α] {s : Set α} : Continuous fun (x : α) => EMetric.infEdist x s

The edist to a set depends continuously on the point

theorem EMetric.infEdist_closure {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} : EMetric.infEdist x (closure s) = EMetric.infEdist x s

The edist to a set and to its closure coincide

theorem EMetric.mem_closure_iff_infEdist_zero {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} : x ∈ closure s ↔ EMetric.infEdist x s = 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} [PseudoEMetricSpace α] {x : α} {s : Set α} (h : IsClosed s) : x ∈ s ↔ EMetric.infEdist 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} [PseudoEMetricSpace α] {x : α} {E : Set α} : 0 < EMetric.infEdist x E ↔ x ∉ closure E

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} [PseudoEMetricSpace α] {x : α} {E : Set α} : 0 < EMetric.infEdist x (closure E) ↔ x ∉ closure E

theorem EMetric.exists_real_pos_lt_infEdist_of_not_mem_closure {α : Type u} [PseudoEMetricSpace α] {x : α} {E : Set α} (h : x ∉ closure E) : ∃ (ε : ℝ), 0 < ε ∧ ENNReal.ofReal ε < EMetric.infEdist x E

theorem EMetric.disjoint_closedBall_of_lt_infEdist {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} {r : ENNReal} (h : r < EMetric.infEdist x s) : Disjoint (EMetric.closedBall x r) s

theorem EMetric.infEdist_image {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {x : α} {t : Set α} {Φ : α → β} (hΦ : Isometry Φ) : EMetric.infEdist (Φ x) (Φ '' t) = EMetric.infEdist x t

The infimum edistance is invariant under isometries

@[simp]

theorem EMetric.infEdist_smul {α : Type u} [PseudoEMetricSpace α] {M : Type u_2} [SMul M α] [IsometricSMul M α] (c : M) (x : α) (s : Set α) : EMetric.infEdist (c • x) (c • s) = EMetric.infEdist x s

@[simp]

theorem EMetric.infEdist_vadd {α : Type u} [PseudoEMetricSpace α] {M : Type u_2} [VAdd M α] [IsometricVAdd M α] (c : M) (x : α) (s : Set α) : EMetric.infEdist (c +ᵥ x) (c +ᵥ s) = EMetric.infEdist x s

theorem IsOpen.exists_iUnion_isClosed {α : Type u} [PseudoEMetricSpace α] {U : Set α} (hU : IsOpen U) : ∃ (F : ℕ → Set α), (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F

theorem IsCompact.exists_infEdist_eq_edist {α : Type u} [PseudoEMetricSpace α] {s : Set α} (hs : IsCompact s) (hne : s.Nonempty) (x : α) : ∃ y ∈ s, EMetric.infEdist x s = edist x y

theorem EMetric.exists_pos_forall_lt_edist {α : Type u} [PseudoEMetricSpace α] {s t : Set α} (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) : ∃ (r : NNReal), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

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

@[irreducible]

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

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

• @EMetric.hausdorffEdist = EMetric.wrapped✝.1

theorem EMetric.hausdorffEdist_def {α : Type u_2} [PseudoEMetricSpace α] (s t : Set α) : EMetric.hausdorffEdist s t = (⨆ x ∈ s, EMetric.infEdist x t) ⊔ ⨆ y ∈ t, EMetric.infEdist y s

@[simp]

theorem EMetric.hausdorffEdist_self {α : Type u} [PseudoEMetricSpace α] {s : Set α} : EMetric.hausdorffEdist s s = 0

The Hausdorff edistance of a set to itself vanishes.

theorem EMetric.hausdorffEdist_comm {α : Type u} [PseudoEMetricSpace α] {s t : Set α} : EMetric.hausdorffEdist s t = EMetric.hausdorffEdist t s

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

theorem EMetric.hausdorffEdist_le_of_infEdist {α : Type u} [PseudoEMetricSpace α] {s t : Set α} {r : ENNReal} (H1 : ∀ x ∈ s, EMetric.infEdist x t ≤ r) (H2 : ∀ x ∈ t, EMetric.infEdist x s ≤ r) : EMetric.hausdorffEdist s t ≤ 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} [PseudoEMetricSpace α] {s t : Set α} {r : ENNReal} (H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r) (H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r) : EMetric.hausdorffEdist s t ≤ 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} [PseudoEMetricSpace α] {x : α} {s t : Set α} (h : x ∈ s) : EMetric.infEdist x t ≤ EMetric.hausdorffEdist s t

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

theorem EMetric.exists_edist_lt_of_hausdorffEdist_lt {α : Type u} [PseudoEMetricSpace α] {x : α} {s t : Set α} {r : ENNReal} (h : x ∈ s) (H : EMetric.hausdorffEdist s t < r) : ∃ y ∈ t, 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} [PseudoEMetricSpace α] {x : α} {s t : Set α} : EMetric.infEdist x t ≤ EMetric.infEdist x s + EMetric.hausdorffEdist s t

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} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {s t : Set α} {Φ : α → β} (h : Isometry Φ) : EMetric.hausdorffEdist (Φ '' s) (Φ '' t) = EMetric.hausdorffEdist s t

The Hausdorff edistance is invariant under isometries.

theorem EMetric.hausdorffEdist_le_ediam {α : Type u} [PseudoEMetricSpace α] {s t : Set α} (hs : s.Nonempty) (ht : t.Nonempty) : EMetric.hausdorffEdist s t ≤ EMetric.diam (s ∪ t)

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

theorem EMetric.hausdorffEdist_triangle {α : Type u} [PseudoEMetricSpace α] {s t u : Set α} : EMetric.hausdorffEdist s u ≤ EMetric.hausdorffEdist s t + EMetric.hausdorffEdist t u

The Hausdorff distance satisfies the triangle inequality.

theorem EMetric.hausdorffEdist_zero_iff_closure_eq_closure {α : Type u} [PseudoEMetricSpace α] {s t : Set α} : EMetric.hausdorffEdist s t = 0 ↔ closure s = closure t

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

@[simp]

theorem EMetric.hausdorffEdist_self_closure {α : Type u} [PseudoEMetricSpace α] {s : Set α} : EMetric.hausdorffEdist s (closure s) = 0

The Hausdorff edistance between a set and its closure vanishes.

@[simp]

theorem EMetric.hausdorffEdist_closure₁ {α : Type u} [PseudoEMetricSpace α] {s t : Set α} : EMetric.hausdorffEdist (closure s) t = EMetric.hausdorffEdist s t

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

@[simp]

theorem EMetric.hausdorffEdist_closure₂ {α : Type u} [PseudoEMetricSpace α] {s t : Set α} : EMetric.hausdorffEdist s (closure t) = EMetric.hausdorffEdist s t

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

theorem EMetric.hausdorffEdist_closure {α : Type u} [PseudoEMetricSpace α] {s t : Set α} : EMetric.hausdorffEdist (closure s) (closure t) = EMetric.hausdorffEdist s t

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

theorem EMetric.hausdorffEdist_zero_iff_eq_of_closed {α : Type u} [PseudoEMetricSpace α] {s t : Set α} (hs : IsClosed s) (ht : IsClosed t) : EMetric.hausdorffEdist s t = 0 ↔ s = t

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

theorem EMetric.hausdorffEdist_empty {α : Type u} [PseudoEMetricSpace α] {s : Set α} (ne : s.Nonempty) : EMetric.hausdorffEdist s ∅ = ⊤

The Haudorff edistance to the empty set is infinite.

theorem EMetric.nonempty_of_hausdorffEdist_ne_top {α : Type u} [PseudoEMetricSpace α] {s t : Set α} (hs : s.Nonempty) (fin : EMetric.hausdorffEdist s t ≠ ⊤) : 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} [PseudoEMetricSpace α] {s t : Set α} (fin : EMetric.hausdorffEdist s t ≠ ⊤) : 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} [PseudoMetricSpace α] (x : α) (s : Set α) : ℝ

The minimal distance of a point to a set

Equations

• Metric.infDist x s = (EMetric.infEdist x s).toReal

theorem Metric.infDist_eq_iInf {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : Metric.infDist x s = ⨅ (y : ↑s), dist x ↑y

theorem Metric.infDist_nonneg {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : 0 ≤ Metric.infDist x s

The minimal distance is always nonnegative

@[simp]

theorem Metric.infDist_empty {α : Type u} [PseudoMetricSpace α] {x : α} : Metric.infDist 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} [PseudoMetricSpace α] {s : Set α} {x : α} (h : s.Nonempty) : EMetric.infEdist x s ≠ ⊤

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

@[simp]

theorem Metric.infEdist_eq_top_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : EMetric.infEdist x s = ⊤ ↔ s = ∅

theorem Metric.infDist_zero_of_mem {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} (h : x ∈ s) : Metric.infDist x s = 0

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

@[simp]

theorem Metric.infDist_singleton {α : Type u} [PseudoMetricSpace α] {x y : α} : Metric.infDist x {y} = dist 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} [PseudoMetricSpace α] {s : Set α} {x y : α} (h : y ∈ s) : Metric.infDist x 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} [PseudoMetricSpace α] {s t : Set α} {x : α} (h : s ⊆ t) (hs : s.Nonempty) : Metric.infDist x t ≤ Metric.infDist x s

The minimal distance is monotone with respect to inclusion.

theorem Metric.infDist_lt_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ} (hs : s.Nonempty) : Metric.infDist x s < r ↔ ∃ y ∈ s, 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} [PseudoMetricSpace α] {s : Set α} {x y : α} : Metric.infDist x s ≤ Metric.infDist y s + 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} [PseudoMetricSpace α] {s : Set α} {x y : α} (h : dist x y < Metric.infDist x s) : y ∉ s

theorem Metric.disjoint_ball_infDist {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : Disjoint (Metric.ball x (Metric.infDist x s)) s

theorem Metric.ball_infDist_subset_compl {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : Metric.ball x (Metric.infDist x s) ⊆ sᶜ

theorem Metric.ball_infDist_compl_subset {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : Metric.ball x (Metric.infDist x sᶜ) ⊆ s

theorem Metric.disjoint_closedBall_of_lt_infDist {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ} (h : r < Metric.infDist x s) : Disjoint (Metric.closedBall x r) s

theorem Metric.dist_le_infDist_add_diam {α : Type u} [PseudoMetricSpace α] {s : Set α} {x y : α} (hs : Bornology.IsBounded s) (hy : y ∈ s) : dist x y ≤ Metric.infDist x s + Metric.diam s

theorem Metric.lipschitz_infDist_pt {α : Type u} [PseudoMetricSpace α] (s : Set α) : LipschitzWith 1 fun (x : α) => Metric.infDist x s

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

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

The minimal distance to a set is uniformly continuous in point

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

The minimal distance to a set is continuous in point

theorem Metric.infDist_closure {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : Metric.infDist x (closure s) = Metric.infDist x s

The minimal distances to a set and its closure coincide.

theorem Metric.infDist_zero_of_mem_closure {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} (hx : x ∈ closure s) : Metric.infDist x s = 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} [PseudoMetricSpace α] {s : Set α} {x : α} (h : s.Nonempty) : x ∈ closure s ↔ Metric.infDist x s = 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} [PseudoMetricSpace α] {s : Set α} {x : α} (h : IsClosed s) (hs : s.Nonempty) : x ∈ s ↔ Metric.infDist 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} [PseudoMetricSpace α] {s : Set α} {x : α} (h : IsClosed s) (hs : s.Nonempty) : x ∉ s ↔ 0 < Metric.infDist x s

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} [PseudoMetricSpace α] {s : Set α} {x : α} (h : x ∉ closure s) : ContinuousAt (fun (x : α) => (Metric.infDist x s)⁻¹) x

theorem Metric.infDist_image {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {t : Set α} {x : α} {Φ : α → β} (hΦ : Isometry Φ) : Metric.infDist (Φ x) (Φ '' t) = Metric.infDist x t

The infimum distance is invariant under isometries.

theorem Metric.infDist_inter_closedBall_of_mem {α : Type u} [PseudoMetricSpace α] {s : Set α} {x y : α} (h : y ∈ s) : Metric.infDist x (s ∩ Metric.closedBall x (dist y x)) = Metric.infDist x s

theorem IsCompact.exists_infDist_eq_dist {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : IsCompact s) (hne : s.Nonempty) (x : α) : ∃ y ∈ s, Metric.infDist x s = dist x y

theorem IsClosed.exists_infDist_eq_dist {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (h : IsClosed s) (hne : s.Nonempty) (x : α) : ∃ y ∈ s, Metric.infDist x s = dist x y

theorem Metric.exists_mem_closure_infDist_eq_dist {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (hne : s.Nonempty) (x : α) : ∃ y ∈ closure s, Metric.infDist x s = dist x y

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

def Metric.infNndist {α : Type u} [PseudoMetricSpace α] (x : α) (s : Set α) : NNReal

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

Equations

• Metric.infNndist x s = (EMetric.infEdist x s).toNNReal

@[simp]

theorem Metric.coe_infNndist {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} : ↑(Metric.infNndist x s) = Metric.infDist x s

theorem Metric.lipschitz_infNndist_pt {α : Type u} [PseudoMetricSpace α] (s : Set α) : LipschitzWith 1 fun (x : α) => Metric.infNndist x s

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

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

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

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

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

The Hausdorff distance as a function into ℝ.

def Metric.hausdorffDist {α : Type u} [PseudoMetricSpace α] (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

• Metric.hausdorffDist s t = (EMetric.hausdorffEdist s t).toReal

theorem Metric.hausdorffDist_nonneg {α : Type u} [PseudoMetricSpace α] {s t : Set α} : 0 ≤ Metric.hausdorffDist s t

The Hausdorff distance is nonnegative.

theorem Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded {α : Type u} [PseudoMetricSpace α] {s t : Set α} (hs : s.Nonempty) (ht : t.Nonempty) (bs : Bornology.IsBounded s) (bt : Bornology.IsBounded t) : EMetric.hausdorffEdist s t ≠ ⊤

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} [PseudoMetricSpace α] {s : Set α} : Metric.hausdorffDist s s = 0

The Hausdorff distance between a set and itself is zero.

theorem Metric.hausdorffDist_comm {α : Type u} [PseudoMetricSpace α] {s t : Set α} : Metric.hausdorffDist s t = Metric.hausdorffDist t s

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

@[simp]

theorem Metric.hausdorffDist_empty {α : Type u} [PseudoMetricSpace α] {s : Set α} : Metric.hausdorffDist s ∅ = 0

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} [PseudoMetricSpace α] {s : Set α} : Metric.hausdorffDist ∅ s = 0

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} [PseudoMetricSpace α] {s t : Set α} {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ x ∈ s, Metric.infDist x t ≤ r) (H2 : ∀ x ∈ t, Metric.infDist x s ≤ r) : Metric.hausdorffDist s t ≤ 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} [PseudoMetricSpace α] {s t : Set α} {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r) (H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r) : Metric.hausdorffDist s t ≤ 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} [PseudoMetricSpace α] {s t : Set α} (hs : s.Nonempty) (bs : Bornology.IsBounded s) (ht : t.Nonempty) (bt : Bornology.IsBounded t) : Metric.hausdorffDist s t ≤ Metric.diam (s ∪ t)

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

theorem Metric.infDist_le_hausdorffDist_of_mem {α : Type u} [PseudoMetricSpace α] {s t : Set α} {x : α} (hx : x ∈ s) (fin : EMetric.hausdorffEdist s t ≠ ⊤) : Metric.infDist x t ≤ Metric.hausdorffDist s t

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

theorem Metric.exists_dist_lt_of_hausdorffDist_lt {α : Type u} [PseudoMetricSpace α] {s t : Set α} {x : α} {r : ℝ} (h : x ∈ s) (H : Metric.hausdorffDist s t < r) (fin : EMetric.hausdorffEdist s t ≠ ⊤) : ∃ y ∈ t, 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} [PseudoMetricSpace α] {s t : Set α} {y : α} {r : ℝ} (h : y ∈ t) (H : Metric.hausdorffDist s t < r) (fin : EMetric.hausdorffEdist s t ≠ ⊤) : ∃ x ∈ s, 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} [PseudoMetricSpace α] {s t : Set α} {x : α} (fin : EMetric.hausdorffEdist s t ≠ ⊤) : Metric.infDist x t ≤ Metric.infDist x s + Metric.hausdorffDist s t

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} [PseudoMetricSpace α] [PseudoMetricSpace β] {s t : Set α} {Φ : α → β} (h : Isometry Φ) : Metric.hausdorffDist (Φ '' s) (Φ '' t) = Metric.hausdorffDist s t

The Hausdorff distance is invariant under isometries.

theorem Metric.hausdorffDist_triangle {α : Type u} [PseudoMetricSpace α] {s t u : Set α} (fin : EMetric.hausdorffEdist s t ≠ ⊤) : Metric.hausdorffDist s u ≤ Metric.hausdorffDist s t + Metric.hausdorffDist t u

The Hausdorff distance satisfies the triangle inequality.

theorem Metric.hausdorffDist_triangle' {α : Type u} [PseudoMetricSpace α] {s t u : Set α} (fin : EMetric.hausdorffEdist t u ≠ ⊤) : Metric.hausdorffDist s u ≤ Metric.hausdorffDist s t + Metric.hausdorffDist t u

The Hausdorff distance satisfies the triangle inequality.

@[simp]

theorem Metric.hausdorffDist_self_closure {α : Type u} [PseudoMetricSpace α] {s : Set α} : Metric.hausdorffDist s (closure s) = 0

The Hausdorff distance between a set and its closure vanishes.

@[simp]

theorem Metric.hausdorffDist_closure₁ {α : Type u} [PseudoMetricSpace α] {s t : Set α} : Metric.hausdorffDist (closure s) t = Metric.hausdorffDist s t

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

@[simp]

theorem Metric.hausdorffDist_closure₂ {α : Type u} [PseudoMetricSpace α] {s t : Set α} : Metric.hausdorffDist s (closure t) = Metric.hausdorffDist s t

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

theorem Metric.hausdorffDist_closure {α : Type u} [PseudoMetricSpace α] {s t : Set α} : Metric.hausdorffDist (closure s) (closure t) = Metric.hausdorffDist s t

The Hausdorff distances between two sets and their closures coincide.

theorem Metric.hausdorffDist_zero_iff_closure_eq_closure {α : Type u} [PseudoMetricSpace α] {s t : Set α} (fin : EMetric.hausdorffEdist s t ≠ ⊤) : Metric.hausdorffDist s t = 0 ↔ closure s = closure t

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

theorem IsClosed.hausdorffDist_zero_iff_eq {α : Type u} [PseudoMetricSpace α] {s t : Set α} (hs : IsClosed s) (ht : IsClosed t) (fin : EMetric.hausdorffEdist s t ≠ ⊤) : Metric.hausdorffDist s t = 0 ↔ s = t

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