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
• Metric.thickening δ s, the open thickening by radius δ of a set s in a pseudo emetric space.
• Metric.cthickening δ s, the closed thickening by radius δ of a set s in a pseudo emetric space.

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 : α) (_ : 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 : α), y ∈ s → d ≤ edist x y

@[simp]

theorem EMetric.infEdist_union {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} {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)

@[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 : Set α} {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, 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_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

@[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

theorem IsOpen.exists_iUnion_isClosed {α : Type u} [PseudoEMetricSpace α] {U : Set α} (hU : IsOpen U) : ∃ F, (∀ (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 : Set.Nonempty s) (x : α) : ∃ y, y ∈ s ∧ EMetric.infEdist x s = edist x y

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

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

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

@[irreducible]

def EMetric.hausdorffEdist {α : Type u_2} [PseudoEMetricSpace α] (s : Set α) (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

@[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 : Set α} {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 : Set α} {t : Set α} {r : ENNReal} (H1 : ∀ (x : α), x ∈ s → EMetric.infEdist x t ≤ r) (H2 : ∀ (x : α), 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 : Set α} {t : Set α} {r : ENNReal} (H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r) (H2 : ∀ (x : α), x ∈ t → ∃ y, 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 : Set α} {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 : Set α} {t : Set α} {r : ENNReal} (h : x ∈ s) (H : EMetric.hausdorffEdist s t < r) : ∃ y, 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 : Set α} {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 : Set α} {t : Set α} {Φ : α → β} (h : Isometry Φ) : EMetric.hausdorffEdist (Φ '' s) (Φ '' t) = EMetric.hausdorffEdist s t

The Hausdorff edistance is invariant under eisometries

theorem EMetric.hausdorffEdist_le_ediam {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hs : Set.Nonempty s) (ht : Set.Nonempty t) : 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 : Set α} {t : Set α} {u : Set α} : EMetric.hausdorffEdist s u ≤ EMetric.hausdorffEdist s t + EMetric.hausdorffEdist t u

The Hausdorff distance satisfies the triangular inequality

theorem EMetric.hausdorffEdist_zero_iff_closure_eq_closure {α : Type u} [PseudoEMetricSpace α] {s : Set α} {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 : Set α} {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 : Set α} {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 : Set α} {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 : Set α} {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 : Set.Nonempty s) : EMetric.hausdorffEdist s ∅ = ⊤

The Haudorff edistance to the empty set is infinite

theorem EMetric.nonempty_of_hausdorffEdist_ne_top {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hs : Set.Nonempty s) (fin : EMetric.hausdorffEdist s t ≠ ⊤) : Set.Nonempty t

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 : Set α} {t : Set α} (fin : EMetric.hausdorffEdist s t ≠ ⊤) : s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t

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 = ENNReal.toReal (EMetric.infEdist x s)

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 : Set.Nonempty s) : EMetric.infEdist x s ≠ ⊤

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

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 : Set α} {t : Set α} {x : α} (h : s ⊆ t) (hs : Set.Nonempty s) : Metric.infDist x t ≤ Metric.infDist x s

The minimal distance is monotonous with respect to inclusion

theorem Metric.infDist_lt_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ} (hs : Set.Nonempty s) : Metric.infDist x s < r ↔ ∃ y, y ∈ s ∧ dist x y < r

The minimal distance to a set is < r iff there exists a point in this set 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 distance 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 : Set.Nonempty s) : 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 : Set.Nonempty s) : 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 : Set.Nonempty s) : ¬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 : Set.Nonempty s) (x : α) : ∃ y, 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 : Set.Nonempty s) (x : α) : ∃ y, y ∈ s ∧ Metric.infDist x s = dist x y

theorem Metric.exists_mem_closure_infDist_eq_dist {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (hne : Set.Nonempty s) (x : α) : ∃ y, 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 = ENNReal.toNNReal (EMetric.infEdist x s)

@[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 : 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

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

theorem Metric.hausdorffDist_nonneg {α : Type u} [PseudoMetricSpace α] {s : Set α} {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 : Set α} {t : Set α} (hs : Set.Nonempty s) (ht : Set.Nonempty t) (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 : Set α} {t : Set α} : Metric.hausdorffDist s t = Metric.hausdorffDist t s

The Hausdorff distance 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 : Set α} {t : Set α} {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ (x : α), x ∈ s → Metric.infDist x t ≤ r) (H2 : ∀ (x : α), 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 : Set α} {t : Set α} {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ r) (H2 : ∀ (x : α), x ∈ t → ∃ y, 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 : Set α} {t : Set α} (hs : Set.Nonempty s) (bs : Bornology.IsBounded s) (ht : Set.Nonempty t) (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 : Set α} {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 : Set α} {t : Set α} {x : α} {r : ℝ} (h : x ∈ s) (H : Metric.hausdorffDist s t < r) (fin : EMetric.hausdorffEdist s t ≠ ⊤) : ∃ y, 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_hausdorffDist_lt' {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} {y : α} {r : ℝ} (h : y ∈ t) (H : Metric.hausdorffDist s t < r) (fin : EMetric.hausdorffEdist s t ≠ ⊤) : ∃ x, 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.infDist_le_infDist_add_hausdorffDist {α : Type u} [PseudoMetricSpace α] {s : Set α} {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 : Set α} {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 : Set α} {t : Set α} {u : Set α} (fin : EMetric.hausdorffEdist s t ≠ ⊤) : Metric.hausdorffDist s u ≤ Metric.hausdorffDist s t + Metric.hausdorffDist t u

The Hausdorff distance satisfies the triangular inequality

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

The Hausdorff distance satisfies the triangular 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 vanish

@[simp]

theorem Metric.hausdorffDist_closure₁ {α : Type u} [PseudoMetricSpace α] {s : Set α} {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 : Set α} {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 : Set α} {t : Set α} : Metric.hausdorffDist (closure s) (closure t) = Metric.hausdorffDist s t

The Hausdorff distance between two sets and their closures coincide

theorem Metric.hausdorffDist_zero_iff_closure_eq_closure {α : Type u} [PseudoMetricSpace α] {s : Set α} {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 : Set α} {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

def Metric.thickening {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : Set α

The (open) δ-thickening Metric.thickening δ E of a subset E in a pseudo emetric space consists of those points that are at distance less than δ from some point of E.

Equations

• Metric.thickening δ E = {x | EMetric.infEdist x E < ENNReal.ofReal δ}

theorem Metric.mem_thickening_iff_infEdist_lt {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α} : x ∈ Metric.thickening δ s ↔ EMetric.infEdist x s < ENNReal.ofReal δ

theorem Metric.eventually_not_mem_thickening_of_infEdist_pos {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : ¬x ∈ closure E) : ∀ᶠ (δ : ℝ) in nhds 0, ¬x ∈ Metric.thickening δ E

An exterior point of a subset E (i.e., a point outside the closure of E) is not in the (open) δ-thickening of E for small enough positive δ.

theorem Metric.thickening_eq_preimage_infEdist {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : Metric.thickening δ E = (fun x => EMetric.infEdist x E) ⁻¹' Set.Iio (ENNReal.ofReal δ)

The (open) thickening equals the preimage of an open interval under EMetric.infEdist.

theorem Metric.isOpen_thickening {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} {E : Set α} : IsOpen (Metric.thickening δ E)

The (open) thickening is an open set.

@[simp]

theorem Metric.thickening_empty {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) : Metric.thickening δ ∅ = ∅

The (open) thickening of the empty set is empty.

theorem Metric.thickening_of_nonpos {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (hδ : δ ≤ 0) (s : Set α) : Metric.thickening δ s = ∅

theorem Metric.thickening_mono {α : Type u} [PseudoEMetricSpace α] {δ₁ : ℝ} {δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : Set α) : Metric.thickening δ₁ E ⊆ Metric.thickening δ₂ E

The (open) thickening Metric.thickening δ E of a fixed subset E is an increasing function of the thickening radius δ.

theorem Metric.thickening_subset_of_subset {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) {E₁ : Set α} {E₂ : Set α} (h : E₁ ⊆ E₂) : Metric.thickening δ E₁ ⊆ Metric.thickening δ E₂

The (open) thickening Metric.thickening δ E with a fixed thickening radius δ is an increasing function of the subset E.

theorem Metric.mem_thickening_iff_exists_edist_lt {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (E : Set α) (x : α) : x ∈ Metric.thickening δ E ↔ ∃ z, z ∈ E ∧ edist x z < ENNReal.ofReal δ

theorem Metric.frontier_thickening_subset {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : ℝ} : frontier (Metric.thickening δ E) ⊆ {x | EMetric.infEdist x E = ENNReal.ofReal δ}

The frontier of the (open) thickening of a set is contained in an EMetric.infEdist level set.

theorem Metric.frontier_thickening_disjoint {α : Type u} [PseudoEMetricSpace α] (A : Set α) : Pairwise (Disjoint on fun r => frontier (Metric.thickening r A))

theorem Metric.mem_thickening_iff_infDist_lt {δ : ℝ} {X : Type u} [PseudoMetricSpace X] {E : Set X} {x : X} (h : Set.Nonempty E) : x ∈ Metric.thickening δ E ↔ Metric.infDist x E < δ

theorem Metric.mem_thickening_iff {δ : ℝ} {X : Type u} [PseudoMetricSpace X] {E : Set X} {x : X} : x ∈ Metric.thickening δ E ↔ ∃ z, z ∈ E ∧ dist x z < δ

A point in a metric space belongs to the (open) δ-thickening of a subset E if and only if it is at distance less than δ from some point of E.

@[simp]

theorem Metric.thickening_singleton {X : Type u} [PseudoMetricSpace X] (δ : ℝ) (x : X) : Metric.thickening δ {x} = Metric.ball x δ

theorem Metric.ball_subset_thickening {X : Type u} [PseudoMetricSpace X] {x : X} {E : Set X} (hx : x ∈ E) (δ : ℝ) : Metric.ball x δ ⊆ Metric.thickening δ E

theorem Metric.thickening_eq_biUnion_ball {X : Type u} [PseudoMetricSpace X] {δ : ℝ} {E : Set X} : Metric.thickening δ E = ⋃ (x : X) (_ : x ∈ E), Metric.ball x δ

The (open) δ-thickening Metric.thickening δ E of a subset E in a metric space equals the union of balls of radius δ centered at points of E.

theorem Bornology.IsBounded.thickening {X : Type u} [PseudoMetricSpace X] {δ : ℝ} {E : Set X} (h : Bornology.IsBounded E) : Bornology.IsBounded (Metric.thickening δ E)

def Metric.cthickening {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : Set α

The closed δ-thickening Metric.cthickening δ E of a subset E in a pseudo emetric space consists of those points that are at infimum distance at most δ from E.

Equations

• Metric.cthickening δ E = {x | EMetric.infEdist x E ≤ ENNReal.ofReal δ}

@[simp]

theorem Metric.mem_cthickening_iff {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α} : x ∈ Metric.cthickening δ s ↔ EMetric.infEdist x s ≤ ENNReal.ofReal δ

theorem Metric.eventually_not_mem_cthickening_of_infEdist_pos {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : ¬x ∈ closure E) : ∀ᶠ (δ : ℝ) in nhds 0, ¬x ∈ Metric.cthickening δ E

An exterior point of a subset E (i.e., a point outside the closure of E) is not in the closed δ-thickening of E for small enough positive δ.

theorem Metric.mem_cthickening_of_edist_le {α : Type u} [PseudoEMetricSpace α] (x : α) (y : α) (δ : ℝ) (E : Set α) (h : y ∈ E) (h' : edist x y ≤ ENNReal.ofReal δ) : x ∈ Metric.cthickening δ E

theorem Metric.mem_cthickening_of_dist_le {α : Type u_2} [PseudoMetricSpace α] (x : α) (y : α) (δ : ℝ) (E : Set α) (h : y ∈ E) (h' : dist x y ≤ δ) : x ∈ Metric.cthickening δ E

theorem Metric.cthickening_eq_preimage_infEdist {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : Metric.cthickening δ E = (fun x => EMetric.infEdist x E) ⁻¹' Set.Iic (ENNReal.ofReal δ)

theorem Metric.isClosed_cthickening {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} {E : Set α} : IsClosed (Metric.cthickening δ E)

The closed thickening is a closed set.

@[simp]

theorem Metric.cthickening_empty {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) : Metric.cthickening δ ∅ = ∅

The closed thickening of the empty set is empty.

theorem Metric.cthickening_of_nonpos {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (hδ : δ ≤ 0) (E : Set α) : Metric.cthickening δ E = closure E

@[simp]

theorem Metric.cthickening_zero {α : Type u} [PseudoEMetricSpace α] (E : Set α) : Metric.cthickening 0 E = closure E

The closed thickening with radius zero is the closure of the set.

theorem Metric.cthickening_max_zero {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : Metric.cthickening (max 0 δ) E = Metric.cthickening δ E

theorem Metric.cthickening_mono {α : Type u} [PseudoEMetricSpace α] {δ₁ : ℝ} {δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : Set α) : Metric.cthickening δ₁ E ⊆ Metric.cthickening δ₂ E

The closed thickening Metric.cthickening δ E of a fixed subset E is an increasing function of the thickening radius δ.

@[simp]

theorem Metric.cthickening_singleton {α : Type u_2} [PseudoMetricSpace α] (x : α) {δ : ℝ} (hδ : 0 ≤ δ) : Metric.cthickening δ {x} = Metric.closedBall x δ

theorem Metric.closedBall_subset_cthickening_singleton {α : Type u_2} [PseudoMetricSpace α] (x : α) (δ : ℝ) : Metric.closedBall x δ ⊆ Metric.cthickening δ {x}

theorem Metric.cthickening_subset_of_subset {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) {E₁ : Set α} {E₂ : Set α} (h : E₁ ⊆ E₂) : Metric.cthickening δ E₁ ⊆ Metric.cthickening δ E₂

The closed thickening Metric.cthickening δ E with a fixed thickening radius δ is an increasing function of the subset E.

theorem Metric.cthickening_subset_thickening {α : Type u} [PseudoEMetricSpace α] {δ₁ : NNReal} {δ₂ : ℝ} (hlt : ↑δ₁ < δ₂) (E : Set α) : Metric.cthickening (↑δ₁) E ⊆ Metric.thickening δ₂ E

theorem Metric.cthickening_subset_thickening' {α : Type u} [PseudoEMetricSpace α] {δ₁ : ℝ} {δ₂ : ℝ} (δ₂_pos : 0 < δ₂) (hlt : δ₁ < δ₂) (E : Set α) : Metric.cthickening δ₁ E ⊆ Metric.thickening δ₂ E

The closed thickening Metric.cthickening δ₁ E is contained in the open thickening Metric.thickening δ₂ E if the radius of the latter is positive and larger.

theorem Metric.thickening_subset_cthickening {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : Metric.thickening δ E ⊆ Metric.cthickening δ E

The open thickening Metric.thickening δ E is contained in the closed thickening Metric.cthickening δ E with the same radius.

theorem Metric.thickening_subset_cthickening_of_le {α : Type u} [PseudoEMetricSpace α] {δ₁ : ℝ} {δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : Set α) : Metric.thickening δ₁ E ⊆ Metric.cthickening δ₂ E

theorem Bornology.IsBounded.cthickening {α : Type u_2} [PseudoMetricSpace α] {δ : ℝ} {E : Set α} (h : Bornology.IsBounded E) : Bornology.IsBounded (Metric.cthickening δ E)

theorem IsCompact.cthickening {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] {s : Set α} (hs : IsCompact s) {r : ℝ} : IsCompact (Metric.cthickening r s)

theorem Metric.thickening_subset_interior_cthickening {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : Metric.thickening δ E ⊆ interior (Metric.cthickening δ E)

theorem Metric.closure_thickening_subset_cthickening {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : closure (Metric.thickening δ E) ⊆ Metric.cthickening δ E

theorem Metric.closure_subset_cthickening {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : closure E ⊆ Metric.cthickening δ E

The closed thickening of a set contains the closure of the set.

theorem Metric.closure_subset_thickening {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) : closure E ⊆ Metric.thickening δ E

The (open) thickening of a set contains the closure of the set.

theorem Metric.self_subset_thickening {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) : E ⊆ Metric.thickening δ E

A set is contained in its own (open) thickening.

theorem Metric.self_subset_cthickening {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (E : Set α) : E ⊆ Metric.cthickening δ E

A set is contained in its own closed thickening.

theorem Metric.thickening_mem_nhdsSet {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : ℝ} (hδ : 0 < δ) : Metric.thickening δ E ∈ nhdsSet E

theorem Metric.cthickening_mem_nhdsSet {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : ℝ} (hδ : 0 < δ) : Metric.cthickening δ E ∈ nhdsSet E

@[simp]

theorem Metric.thickening_union {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (s : Set α) (t : Set α) : Metric.thickening δ (s ∪ t) = Metric.thickening δ s ∪ Metric.thickening δ t

@[simp]

theorem Metric.cthickening_union {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (s : Set α) (t : Set α) : Metric.cthickening δ (s ∪ t) = Metric.cthickening δ s ∪ Metric.cthickening δ t

@[simp]

theorem Metric.thickening_iUnion {ι : Sort u_1} {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (f : ι → Set α) : Metric.thickening δ (⋃ (i : ι), f i) = ⋃ (i : ι), Metric.thickening δ (f i)

theorem Metric.ediam_cthickening_le {α : Type u} [PseudoEMetricSpace α] {s : Set α} (ε : NNReal) : EMetric.diam (Metric.cthickening (↑ε) s) ≤ EMetric.diam s + 2 * ↑ε

theorem Metric.ediam_thickening_le {α : Type u} [PseudoEMetricSpace α] {s : Set α} (ε : NNReal) : EMetric.diam (Metric.thickening (↑ε) s) ≤ EMetric.diam s + 2 * ↑ε

theorem Metric.diam_cthickening_le {ε : ℝ} {α : Type u_2} [PseudoMetricSpace α] (s : Set α) (hε : 0 ≤ ε) : Metric.diam (Metric.cthickening ε s) ≤ Metric.diam s + 2 * ε

theorem Metric.diam_thickening_le {ε : ℝ} {α : Type u_2} [PseudoMetricSpace α] (s : Set α) (hε : 0 ≤ ε) : Metric.diam (Metric.thickening ε s) ≤ Metric.diam s + 2 * ε

@[simp]

theorem Metric.thickening_closure {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} {s : Set α} : Metric.thickening δ (closure s) = Metric.thickening δ s

@[simp]

theorem Metric.cthickening_closure {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} {s : Set α} : Metric.cthickening δ (closure s) = Metric.cthickening δ s

theorem Disjoint.exists_thickenings {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hst : Disjoint s t) (hs : IsCompact s) (ht : IsClosed t) : ∃ δ, 0 < δ ∧ Disjoint (Metric.thickening δ s) (Metric.thickening δ t)

theorem Disjoint.exists_cthickenings {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hst : Disjoint s t) (hs : IsCompact s) (ht : IsClosed t) : ∃ δ, 0 < δ ∧ Disjoint (Metric.cthickening δ s) (Metric.cthickening δ t)

theorem IsCompact.exists_cthickening_subset_open {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsOpen t) (hst : s ⊆ t) : ∃ δ, 0 < δ ∧ Metric.cthickening δ s ⊆ t

theorem IsCompact.exists_isCompact_cthickening {α : Type u} [PseudoEMetricSpace α] {s : Set α} [LocallyCompactSpace α] (hs : IsCompact s) : ∃ δ, 0 < δ ∧ IsCompact (Metric.cthickening δ s)

theorem IsCompact.exists_thickening_subset_open {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsOpen t) (hst : s ⊆ t) : ∃ δ, 0 < δ ∧ Metric.thickening δ s ⊆ t

theorem Metric.hasBasis_nhdsSet_thickening {α : Type u} [PseudoEMetricSpace α] {K : Set α} (hK : IsCompact K) : Filter.HasBasis (nhdsSet K) (fun δ => 0 < δ) fun δ => Metric.thickening δ K

theorem Metric.hasBasis_nhdsSet_cthickening {α : Type u} [PseudoEMetricSpace α] {K : Set α} (hK : IsCompact K) : Filter.HasBasis (nhdsSet K) (fun δ => 0 < δ) fun δ => Metric.cthickening δ K

theorem Metric.cthickening_eq_iInter_cthickening' {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (s : Set ℝ) (hsδ : s ⊆ Set.Ioi δ) (hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Set.Ioc δ ε)) (E : Set α) : Metric.cthickening δ E = ⋂ (ε : ℝ) (_ : ε ∈ s), Metric.cthickening ε E

theorem Metric.cthickening_eq_iInter_cthickening {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (E : Set α) : Metric.cthickening δ E = ⋂ (ε : ℝ) (_ : δ < ε), Metric.cthickening ε E

theorem Metric.cthickening_eq_iInter_thickening' {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (δ_nn : 0 ≤ δ) (s : Set ℝ) (hsδ : s ⊆ Set.Ioi δ) (hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Set.Ioc δ ε)) (E : Set α) : Metric.cthickening δ E = ⋂ (ε : ℝ) (_ : ε ∈ s), Metric.thickening ε E

theorem Metric.cthickening_eq_iInter_thickening {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (δ_nn : 0 ≤ δ) (E : Set α) : Metric.cthickening δ E = ⋂ (ε : ℝ) (_ : δ < ε), Metric.thickening ε E

theorem Metric.cthickening_eq_iInter_thickening'' {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : Metric.cthickening δ E = ⋂ (ε : ℝ) (_ : max 0 δ < ε), Metric.thickening ε E

theorem Metric.closure_eq_iInter_cthickening' {α : Type u} [PseudoEMetricSpace α] (E : Set α) (s : Set ℝ) (hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Set.Ioc 0 ε)) : closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), Metric.cthickening δ E

The closure of a set equals the intersection of its closed thickenings of positive radii accumulating at zero.

theorem Metric.closure_eq_iInter_cthickening {α : Type u} [PseudoEMetricSpace α] (E : Set α) : closure E = ⋂ (δ : ℝ) (_ : 0 < δ), Metric.cthickening δ E

The closure of a set equals the intersection of its closed thickenings of positive radii.

theorem Metric.closure_eq_iInter_thickening' {α : Type u} [PseudoEMetricSpace α] (E : Set α) (s : Set ℝ) (hs₀ : s ⊆ Set.Ioi 0) (hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Set.Ioc 0 ε)) : closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), Metric.thickening δ E

The closure of a set equals the intersection of its open thickenings of positive radii accumulating at zero.

theorem Metric.closure_eq_iInter_thickening {α : Type u} [PseudoEMetricSpace α] (E : Set α) : closure E = ⋂ (δ : ℝ) (_ : 0 < δ), Metric.thickening δ E

The closure of a set equals the intersection of its (open) thickenings of positive radii.

theorem Metric.frontier_cthickening_subset {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : ℝ} : frontier (Metric.cthickening δ E) ⊆ {x | EMetric.infEdist x E = ENNReal.ofReal δ}

The frontier of the closed thickening of a set is contained in an EMetric.infEdist level set.

theorem Metric.closedBall_subset_cthickening {α : Type u_2} [PseudoMetricSpace α] {x : α} {E : Set α} (hx : x ∈ E) (δ : ℝ) : Metric.closedBall x δ ⊆ Metric.cthickening δ E

The closed ball of radius δ centered at a point of E is included in the closed thickening of E.

theorem Metric.cthickening_subset_iUnion_closedBall_of_lt {α : Type u_2} [PseudoMetricSpace α] (E : Set α) {δ : ℝ} {δ' : ℝ} (hδ₀ : 0 < δ') (hδδ' : δ < δ') : Metric.cthickening δ E ⊆ ⋃ (x : α) (_ : x ∈ E), Metric.closedBall x δ'

theorem IsCompact.cthickening_eq_biUnion_closedBall {α : Type u_2} [PseudoMetricSpace α] {δ : ℝ} {E : Set α} (hE : IsCompact E) (hδ : 0 ≤ δ) : Metric.cthickening δ E = ⋃ (x : α) (_ : x ∈ E), Metric.closedBall x δ

The closed thickening of a compact set E is the union of the balls Metric.closedBall x δ over x ∈ E.

See also Metric.cthickening_eq_biUnion_closedBall.

theorem Metric.cthickening_eq_biUnion_closedBall {δ : ℝ} {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] (E : Set α) (hδ : 0 ≤ δ) : Metric.cthickening δ E = ⋃ (x : α) (_ : x ∈ closure E), Metric.closedBall x δ

theorem IsClosed.cthickening_eq_biUnion_closedBall {δ : ℝ} {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] {E : Set α} (hE : IsClosed E) (hδ : 0 ≤ δ) : Metric.cthickening δ E = ⋃ (x : α) (_ : x ∈ E), Metric.closedBall x δ

theorem Metric.infEdist_le_infEdist_cthickening_add {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α} : EMetric.infEdist x s ≤ EMetric.infEdist x (Metric.cthickening δ s) + ENNReal.ofReal δ

For the equality, see infEdist_cthickening.

theorem Metric.infEdist_le_infEdist_thickening_add {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α} : EMetric.infEdist x s ≤ EMetric.infEdist x (Metric.thickening δ s) + ENNReal.ofReal δ

For the equality, see infEdist_thickening.

@[simp]

theorem Metric.thickening_thickening_subset {α : Type u} [PseudoEMetricSpace α] (ε : ℝ) (δ : ℝ) (s : Set α) : Metric.thickening ε (Metric.thickening δ s) ⊆ Metric.thickening (ε + δ) s

For the equality, see thickening_thickening.

@[simp]

theorem Metric.thickening_cthickening_subset {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (ε : ℝ) (hδ : 0 ≤ δ) (s : Set α) : Metric.thickening ε (Metric.cthickening δ s) ⊆ Metric.thickening (ε + δ) s

For the equality, see thickening_cthickening.

@[simp]

theorem Metric.cthickening_thickening_subset {α : Type u} [PseudoEMetricSpace α] {ε : ℝ} (hε : 0 ≤ ε) (δ : ℝ) (s : Set α) : Metric.cthickening ε (Metric.thickening δ s) ⊆ Metric.cthickening (ε + δ) s

For the equality, see cthickening_thickening.

@[simp]

theorem Metric.cthickening_cthickening_subset {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} {ε : ℝ} (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (s : Set α) : Metric.cthickening ε (Metric.cthickening δ s) ⊆ Metric.cthickening (ε + δ) s

For the equality, see cthickening_cthickening.

theorem Metric.frontier_cthickening_disjoint {α : Type u} [PseudoEMetricSpace α] (A : Set α) : Pairwise (Disjoint on fun r => frontier (Metric.cthickening (↑r) A))