# Documentation

Mathlib.Topology.MetricSpace.HausdorffDistance

# 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} (x : α) (s : Set α) :

The minimal edistance of a point to a set

Instances For
@[simp]
theorem EMetric.infEdist_empty {α : Type u} {x : α} :
theorem EMetric.le_infEdist {α : Type u} {x : α} {s : Set α} {d : ENNReal} :
d ∀ (y : α), y sd 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)
@[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 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} {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.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, (∀ (n : ), IsClosed (F n)) (∀ (n : ), F n U) ⋃ (n : ), F n = U
theorem IsCompact.exists_infEdist_eq_edist {α : Type u} {s : Set α} (hs : ) (hne : ) (x : α) :
y, y s = edist x y
theorem EMetric.exists_pos_forall_lt_edist {α : Type u} {s : Set α} {t : Set α} (hs : ) (ht : ) (hst : Disjoint s t) :
r, 0 < r ∀ (x : α), x s∀ (y : α), y tr < edist x y

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

theorem EMetric.hausdorffEdist_def {α : Type u_2} (s : Set α) (t : Set α) :
= (⨆ (x : α) (_ : x s), ) ⨆ (y : α) (_ : y t),
@[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

Instances For
@[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 : ∀ (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.hausdorffEdist_le_of_mem_edist {α : Type u} {s : Set α} {t : Set α} {r : ENNReal} (H1 : ∀ (x : α), x sy, y t edist x y r) (H2 : ∀ (x : α), x ty, y s 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 : ) :
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} {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 eisometries

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

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 triangular 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 : ) :

The Haudorff edistance to the empty set is infinite

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

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 =

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

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

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

The minimal distance is monotonous with respect to inclusion

theorem Metric.infDist_lt_iff {α : Type u} {s : Set α} {x : α} {r : } (hs : ) :
< 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} {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 < ) :
¬y s
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 α) :

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 distance 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 : ) :
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 : ) :
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 : ) :
¬x s 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 => ()⁻¹) 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 : ) (x : α) :
y, y s = dist x y
theorem IsClosed.exists_infDist_eq_dist {α : Type u} {s : Set α} [] (h : ) (hne : ) (x : α) :
y, y s = dist x y
theorem Metric.exists_mem_closure_infDist_eq_dist {α : Type u} {s : Set α} [] (hne : ) (x : α) :
y, 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

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

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

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 : ) (ht : ) (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 distance 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 : ∀ (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.hausdorffDist_le_of_mem_dist {α : Type u} {s : Set α} {t : Set α} {r : } (hr : 0 r) (H1 : ∀ (x : α), x sy, y t dist x y r) (H2 : ∀ (x : α), x ty, 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.hausdorffDist_le_diam {α : Type u} {s : Set α} {t : Set α} (hs : ) (bs : ) (ht : ) (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 : ) :
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} {s : Set α} {t : Set α} {y : α} {r : } (h : y t) (H : ) (fin : ) :
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} {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 triangular inequality

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

The Hausdorff distance satisfies the triangular inequality

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

The Hausdorff distance between a set and its closure vanish

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

def Metric.thickening {α : Type u} (δ : ) (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.

Instances For
theorem Metric.mem_thickening_iff_infEdist_lt {α : Type u} {δ : } {s : Set α} {x : α} :
x
theorem Metric.eventually_not_mem_thickening_of_infEdist_pos {α : Type u} {E : Set α} {x : α} (h : ¬x ) :
∀ᶠ (δ : ) in nhds 0, ¬x

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} (δ : ) (E : Set α) :
= (fun x => ) ⁻¹'

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

theorem Metric.isOpen_thickening {α : Type u} {δ : } {E : Set α} :

The (open) thickening is an open set.

@[simp]
theorem Metric.thickening_empty {α : Type u} (δ : ) :

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

theorem Metric.thickening_of_nonpos {α : Type u} {δ : } (hδ : δ 0) (s : Set α) :
theorem Metric.thickening_mono {α : Type u} {δ₁ : } {δ₂ : } (hle : δ₁ δ₂) (E : Set α) :

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} (δ : ) {E₁ : Set α} {E₂ : Set α} (h : E₁ 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} {δ : } (E : Set α) (x : α) :
x z, z E edist x z <
theorem Metric.frontier_thickening_subset {α : Type u} (E : Set α) {δ : } :
{x | }

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

theorem Metric.frontier_thickening_disjoint {α : Type u} (A : Set α) :
Pairwise (Disjoint on fun r => )
theorem Metric.mem_thickening_iff_infDist_lt {δ : } {X : Type u} {E : Set X} {x : X} (h : ) :
x < δ
theorem Metric.mem_thickening_iff {δ : } {X : Type u} {E : Set X} {x : X} :
x 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} (δ : ) (x : X) :
=
theorem Metric.ball_subset_thickening {X : Type u} {x : X} {E : Set X} (hx : x E) (δ : ) :
theorem Metric.thickening_eq_biUnion_ball {X : Type u} {δ : } {E : Set X} :
= ⋃ (x : X) (_ : x E),

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} {δ : } {E : Set X} (h : ) :
def Metric.cthickening {α : Type u} (δ : ) (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.

Instances For
@[simp]
theorem Metric.mem_cthickening_iff {α : Type u} {δ : } {s : Set α} {x : α} :
x
theorem Metric.eventually_not_mem_cthickening_of_infEdist_pos {α : Type u} {E : Set α} {x : α} (h : ¬x ) :
∀ᶠ (δ : ) in nhds 0, ¬x

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} (x : α) (y : α) (δ : ) (E : Set α) (h : y E) (h' : edist x y ) :
x
theorem Metric.mem_cthickening_of_dist_le {α : Type u_2} (x : α) (y : α) (δ : ) (E : Set α) (h : y E) (h' : dist x y δ) :
x
theorem Metric.cthickening_eq_preimage_infEdist {α : Type u} (δ : ) (E : Set α) :
= (fun x => ) ⁻¹'
theorem Metric.isClosed_cthickening {α : Type u} {δ : } {E : Set α} :

The closed thickening is a closed set.

@[simp]
theorem Metric.cthickening_empty {α : Type u} (δ : ) :

The closed thickening of the empty set is empty.

theorem Metric.cthickening_of_nonpos {α : Type u} {δ : } (hδ : δ 0) (E : Set α) :
@[simp]
theorem Metric.cthickening_zero {α : Type u} (E : Set α) :

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

theorem Metric.cthickening_max_zero {α : Type u} (δ : ) (E : Set α) :
theorem Metric.cthickening_mono {α : Type u} {δ₁ : } {δ₂ : } (hle : δ₁ δ₂) (E : Set α) :

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} (x : α) {δ : } (hδ : 0 δ) :
=
theorem Metric.cthickening_subset_of_subset {α : Type u} (δ : ) {E₁ : Set α} {E₂ : Set α} (h : E₁ 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} {δ₁ : NNReal} {δ₂ : } (hlt : δ₁ < δ₂) (E : Set α) :
Metric.cthickening (δ₁) E
theorem Metric.cthickening_subset_thickening' {α : Type u} {δ₁ : } {δ₂ : } (δ₂_pos : 0 < δ₂) (hlt : δ₁ < δ₂) (E : Set α) :

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} (δ : ) (E : Set α) :

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} {δ₁ : } {δ₂ : } (hle : δ₁ δ₂) (E : Set α) :
theorem Bornology.IsBounded.cthickening {α : Type u_2} {δ : } {E : Set α} (h : ) :
theorem IsCompact.cthickening {α : Type u_2} [] {s : Set α} (hs : ) {r : } :
theorem Metric.closure_subset_cthickening {α : Type u} (δ : ) (E : Set α) :

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

theorem Metric.closure_subset_thickening {α : Type u} {δ : } (δ_pos : 0 < δ) (E : Set α) :

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

theorem Metric.self_subset_thickening {α : Type u} {δ : } (δ_pos : 0 < δ) (E : Set α) :
E

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

theorem Metric.self_subset_cthickening {α : Type u} {δ : } (E : Set α) :
E

A set is contained in its own closed thickening.

theorem Metric.thickening_mem_nhdsSet {α : Type u} (E : Set α) {δ : } (hδ : 0 < δ) :
theorem Metric.cthickening_mem_nhdsSet {α : Type u} (E : Set α) {δ : } (hδ : 0 < δ) :
@[simp]
theorem Metric.thickening_union {α : Type u} (δ : ) (s : Set α) (t : Set α) :
@[simp]
theorem Metric.cthickening_union {α : Type u} (δ : ) (s : Set α) (t : Set α) :
@[simp]
theorem Metric.thickening_iUnion {ι : Sort u_1} {α : Type u} (δ : ) (f : ιSet α) :
Metric.thickening δ (⋃ (i : ι), f i) = ⋃ (i : ι), Metric.thickening δ (f i)
theorem Metric.ediam_cthickening_le {α : Type u} {s : Set α} (ε : NNReal) :
EMetric.diam (Metric.cthickening (ε) s) + 2 * ε
theorem Metric.ediam_thickening_le {α : Type u} {s : Set α} (ε : NNReal) :
EMetric.diam (Metric.thickening (ε) s) + 2 * ε
theorem Metric.diam_cthickening_le {ε : } {α : Type u_2} (s : Set α) (hε : 0 ε) :
+ 2 * ε
theorem Metric.diam_thickening_le {ε : } {α : Type u_2} (s : Set α) (hε : 0 ε) :
+ 2 * ε
@[simp]
theorem Metric.thickening_closure {α : Type u} {δ : } {s : Set α} :
=
@[simp]
theorem Metric.cthickening_closure {α : Type u} {δ : } {s : Set α} :
=
theorem Disjoint.exists_thickenings {α : Type u} {s : Set α} {t : Set α} (hst : Disjoint s t) (hs : ) (ht : ) :
δ, 0 < δ Disjoint () ()
theorem Disjoint.exists_cthickenings {α : Type u} {s : Set α} {t : Set α} (hst : Disjoint s t) (hs : ) (ht : ) :
δ, 0 < δ Disjoint () ()
theorem IsCompact.exists_cthickening_subset_open {α : Type u} {s : Set α} {t : Set α} (hs : ) (ht : ) (hst : s t) :
δ, 0 < δ t
theorem IsCompact.exists_isCompact_cthickening {α : Type u} {s : Set α} (hs : ) :
δ, 0 < δ
theorem IsCompact.exists_thickening_subset_open {α : Type u} {s : Set α} {t : Set α} (hs : ) (ht : ) (hst : s t) :
δ, 0 < δ t
theorem Metric.hasBasis_nhdsSet_thickening {α : Type u} {K : Set α} (hK : ) :
Filter.HasBasis () (fun δ => 0 < δ) fun δ =>
theorem Metric.hasBasis_nhdsSet_cthickening {α : Type u} {K : Set α} (hK : ) :
Filter.HasBasis () (fun δ => 0 < δ) fun δ =>
theorem Metric.cthickening_eq_iInter_cthickening' {α : Type u} {δ : } (s : ) (hsδ : s ) (hs : ∀ (ε : ), δ < εSet.Nonempty (s Set.Ioc δ ε)) (E : Set α) :
= ⋂ (ε : ) (_ : ε s),
theorem Metric.cthickening_eq_iInter_cthickening {α : Type u} {δ : } (E : Set α) :
= ⋂ (ε : ) (_ : δ < ε),
theorem Metric.cthickening_eq_iInter_thickening' {α : Type u} {δ : } (δ_nn : 0 δ) (s : ) (hsδ : s ) (hs : ∀ (ε : ), δ < εSet.Nonempty (s Set.Ioc δ ε)) (E : Set α) :
= ⋂ (ε : ) (_ : ε s),
theorem Metric.cthickening_eq_iInter_thickening {α : Type u} {δ : } (δ_nn : 0 δ) (E : Set α) :
= ⋂ (ε : ) (_ : δ < ε),
theorem Metric.cthickening_eq_iInter_thickening'' {α : Type u} (δ : ) (E : Set α) :
= ⋂ (ε : ) (_ : max 0 δ < ε),
theorem Metric.closure_eq_iInter_cthickening' {α : Type u} (E : Set α) (s : ) (hs : ∀ (ε : ), 0 < εSet.Nonempty (s Set.Ioc 0 ε)) :
= ⋂ (δ : ) (_ : δ s),

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} (E : Set α) :
= ⋂ (δ : ) (_ : 0 < δ),

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

theorem Metric.closure_eq_iInter_thickening' {α : Type u} (E : Set α) (s : ) (hs₀ : s ) (hs : ∀ (ε : ), 0 < εSet.Nonempty (s Set.Ioc 0 ε)) :
= ⋂ (δ : ) (_ : δ s),

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} (E : Set α) :
= ⋂ (δ : ) (_ : 0 < δ),

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

theorem Metric.frontier_cthickening_subset {α : Type u} (E : Set α) {δ : } :
{x | }

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} {x : α} {E : Set α} (hx : x 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} (E : Set α) {δ : } {δ' : } (hδ₀ : 0 < δ') (hδδ' : δ < δ') :
⋃ (x : α) (_ : x E),
theorem IsCompact.cthickening_eq_biUnion_closedBall {α : Type u_2} {δ : } {E : Set α} (hE : ) (hδ : 0 δ) :
= ⋃ (x : α) (_ : x E),

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} [] (E : Set α) (hδ : 0 δ) :
= ⋃ (x : α) (_ : x ),
theorem IsClosed.cthickening_eq_biUnion_closedBall {δ : } {α : Type u_2} [] {E : Set α} (hE : ) (hδ : 0 δ) :
= ⋃ (x : α) (_ : x E),
theorem Metric.infEdist_le_infEdist_cthickening_add {α : Type u} {δ : } {s : Set α} {x : α} :

For the equality, see infEdist_cthickening.

theorem Metric.infEdist_le_infEdist_thickening_add {α : Type u} {δ : } {s : Set α} {x : α} :

For the equality, see infEdist_thickening.

@[simp]
theorem Metric.thickening_thickening_subset {α : Type u} (ε : ) (δ : ) (s : Set α) :

For the equality, see thickening_thickening.

@[simp]
theorem Metric.thickening_cthickening_subset {α : Type u} {δ : } (ε : ) (hδ : 0 δ) (s : Set α) :

For the equality, see thickening_cthickening.

@[simp]
theorem Metric.cthickening_thickening_subset {α : Type u} {ε : } (hε : 0 ε) (δ : ) (s : Set α) :

For the equality, see cthickening_thickening.

@[simp]
theorem Metric.cthickening_cthickening_subset {α : Type u} {δ : } {ε : } (hε : 0 ε) (hδ : 0 δ) (s : Set α) :

For the equality, see cthickening_cthickening.

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