# mathlibdocumentation

topology.metric_space.hausdorff_distance

# Hausdorff distance #

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

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

## Main definitions #

This files introduces:

• `inf_edist x s`, the infimum edistance of a point `x` to a set `s` in an emetric space
• `Hausdorff_edist s t`, the Hausdorff edistance of two sets in an emetric space
• Versions of these notions on metric spaces, called respectively `inf_dist` and `Hausdorff_dist`
• `thickening δ s`, the open thickening by radius `δ` of a set `s` in a pseudo emetric space.
• `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∞`. #

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

The minimal edistance of a point to a set

Equations
@[simp]
theorem emetric.inf_edist_empty {α : Type u} {x : α} :
theorem emetric.le_inf_edist {α : Type u} {x : α} {s : set α} {d : ennreal} :
d (y : α), y s d
@[simp]
theorem emetric.inf_edist_union {α : Type u} {x : α} {s t : set α} :
(s t) =

The edist to a union is the minimum of the edists

@[simp]
theorem emetric.inf_edist_Union {ι : Sort u_1} {α : Type u} (f : ι set α) (x : α) :
( (i : ι), f i) = (i : ι), (f i)
@[simp]
theorem emetric.inf_edist_singleton {α : Type u} {x y : α} :
{y} =

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

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

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

theorem emetric.inf_edist_zero_of_mem {α : Type u} {x : α} {s : set α} (h : x s) :
= 0

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

theorem emetric.inf_edist_anti {α : Type u} {x : α} {s t : set α} (h : s t) :

The edist is antitone with respect to inclusion.

theorem emetric.inf_edist_lt_iff {α : Type u} {x : α} {s : set α} {r : ennreal} :
< r (y : α) (H : y s), < r

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

theorem emetric.inf_edist_le_inf_edist_add_edist {α : Type u} {x y : α} {s : set α} :

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.inf_edist_le_edist_add_inf_edist {α : Type u} {x y : α} {s : set α} :
theorem emetric.edist_le_inf_edist_add_ediam {α : Type u} {x y : α} {s : set α} (hy : y s) :
@[continuity]
theorem emetric.continuous_inf_edist {α : Type u} {s : set α} :
continuous (λ (x : α),

The edist to a set depends continuously on the point

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

The edist to a set and to its closure coincide

theorem emetric.mem_closure_iff_inf_edist_zero {α : Type u} {x : α} {s : set α} :
x = 0

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

theorem emetric.mem_iff_inf_edist_zero_of_closed {α : Type u} {x : α} {s : set α} (h : is_closed s) :
x s = 0

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

theorem emetric.inf_edist_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.inf_edist_closure_pos_iff_not_mem_closure {α : Type u} {x : α} {E : set α} :
0 < (closure E) x
theorem emetric.exists_real_pos_lt_inf_edist_of_not_mem_closure {α : Type u} {x : α} {E : set α} (h : x ) :
(ε : ), 0 < ε
theorem emetric.disjoint_closed_ball_of_lt_inf_edist {α : Type u} {x : α} {s : set α} {r : ennreal} (h : r < ) :
s
theorem emetric.inf_edist_image {α : Type u} {β : Type v} {x : α} {t : set α} {Φ : α β} (hΦ : isometry Φ) :
emetric.inf_edist (Φ x) '' t) =

The infimum edistance is invariant under isometries

theorem is_open.exists_Union_is_closed {α : Type u} {U : set α} (hU : is_open U) :
(F : set α), ( (n : ), is_closed (F n)) ( (n : ), F n U) ( (n : ), F n) = U
theorem is_compact.exists_inf_edist_eq_edist {α : Type u} {s : set α} (hs : is_compact s) (hne : s.nonempty) (x : α) :
(y : α) (H : y s),
theorem emetric.exists_pos_forall_lt_edist {α : Type u} {s t : set α} (hs : is_compact s) (ht : is_closed t) (hst : t) :
(r : nnreal), 0 < r (x : α), x s (y : α), y t r <

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

@[irreducible]
noncomputable def emetric.Hausdorff_edist {α : Type u} (s t : set α) :

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

Equations
theorem emetric.Hausdorff_edist_def {α : Type u} (s t : set α) :
= ( (x : α) (H : x s), (y : α) (H : y t),
@[simp]
theorem emetric.Hausdorff_edist_self {α : Type u} {s : set α} :

The Hausdorff edistance of a set to itself vanishes

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

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

theorem emetric.Hausdorff_edist_le_of_inf_edist {α : Type u} {s t : set α} {r : 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.Hausdorff_edist_le_of_mem_edist {α : Type u} {s t : set α} {r : ennreal} (H1 : (x : α), x s ( (y : α) (H : y t), r)) (H2 : (x : α), x t ( (y : α) (H : y s), r)) :

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

theorem emetric.inf_edist_le_Hausdorff_edist_of_mem {α : Type u} {x : α} {s t : set α} (h : x s) :

The distance to a set is controlled by the Hausdorff distance

theorem emetric.exists_edist_lt_of_Hausdorff_edist_lt {α : Type u} {x : α} {s t : set α} {r : ennreal} (h : x s) (H : < r) :
(y : α) (H : y t), < r

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

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

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

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

The Hausdorff edistance is invariant under eisometries

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

The Hausdorff distance is controlled by the diameter of the union

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

The Hausdorff distance satisfies the triangular inequality

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

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

The Hausdorff edistance between a set and its closure vanishes

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

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

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

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

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

The Hausdorff edistance between sets or their closures is the same

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

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

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

The Haudorff edistance to the empty set is infinite

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

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

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

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

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

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

The minimal distance of a point to a set

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

the minimal distance is always nonnegative

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

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

theorem metric.inf_edist_ne_top {α : Type u} {s : set α} {x : α} (h : s.nonempty) :

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

theorem metric.inf_dist_zero_of_mem {α : Type u} {s : set α} {x : α} (h : x s) :
= 0

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

@[simp]
theorem metric.inf_dist_singleton {α : Type u} {x y : α} :
{y} =

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

theorem metric.inf_dist_le_dist_of_mem {α : Type u} {s : set α} {x y : α} (h : y s) :

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

theorem metric.inf_dist_le_inf_dist_of_subset {α : Type u} {s t : set α} {x : α} (h : s t) (hs : s.nonempty) :

The minimal distance is monotonous with respect to inclusion

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

The minimal distance to a set is `< r` iff there exists a point in this set at distance `< r`

theorem metric.inf_dist_le_inf_dist_add_dist {α : Type u} {s : set α} {x y : α} :
+

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_inf_dist {α : Type u} {s : set α} {x y : α} (h : < ) :
y s
theorem metric.disjoint_ball_inf_dist {α : Type u} {s : set α} {x : α} :
disjoint s)) s
theorem metric.ball_inf_dist_subset_compl {α : Type u} {s : set α} {x : α} :
s) s
theorem metric.ball_inf_dist_compl_subset {α : Type u} {s : set α} {x : α} :
s) s
theorem metric.disjoint_closed_ball_of_lt_inf_dist {α : Type u} {s : set α} {x : α} {r : } (h : r < ) :
s
theorem metric.dist_le_inf_dist_add_diam {α : Type u} {s : set α} {x y : α} (hs : metric.bounded s) (hy : y s) :
theorem metric.lipschitz_inf_dist_pt {α : Type u} (s : set α) :
(λ (x : α), s)

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

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

The minimal distance to a set is uniformly continuous in point

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

The minimal distance to a set is continuous in point

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

The minimal distance to a set and its closure coincide

theorem metric.inf_dist_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 `mem_closure_iff_inf_dist_zero`.

theorem metric.mem_closure_iff_inf_dist_zero {α : Type u} {s : set α} {x : α} (h : s.nonempty) :
x = 0

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

theorem is_closed.mem_iff_inf_dist_zero {α : Type u} {s : set α} {x : α} (h : is_closed s) (hs : s.nonempty) :
x s = 0

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

theorem is_closed.not_mem_iff_inf_dist_pos {α : Type u} {s : set α} {x : α} (h : is_closed s) (hs : s.nonempty) :
x s 0 <

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

theorem metric.inf_dist_image {α : Type u} {β : Type v} {t : set α} {x : α} {Φ : α β} (hΦ : isometry Φ) :
metric.inf_dist (Φ x) '' t) =

The infimum distance is invariant under isometries

theorem metric.inf_dist_inter_closed_ball_of_mem {α : Type u} {s : set α} {x y : α} (h : y s) :
(s x)) =
theorem is_compact.exists_inf_dist_eq_dist {α : Type u} {s : set α} (h : is_compact s) (hne : s.nonempty) (x : α) :
(y : α) (H : y s), =
theorem is_closed.exists_inf_dist_eq_dist {α : Type u} {s : set α} [proper_space α] (h : is_closed s) (hne : s.nonempty) (x : α) :
(y : α) (H : y s), =
theorem metric.exists_mem_closure_inf_dist_eq_dist {α : Type u} {s : set α} [proper_space α] (hne : s.nonempty) (x : α) :
(y : α) (H : y closure s), =

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

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

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

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

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

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

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

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

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

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

noncomputable def metric.Hausdorff_dist {α : Type u} (s t : set α) :

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

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

The Hausdorff distance is nonnegative

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

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

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

The Hausdorff distance between a set and itself is zero

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

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

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

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

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

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

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

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

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

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

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

The Hausdorff distance is controlled by the diameter of the union

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

The distance to a set is controlled by the Hausdorff distance

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

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

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

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

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

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

theorem metric.Hausdorff_dist_image {α : Type u} {β : Type v} {s t : set α} {Φ : α β} (h : isometry Φ) :
metric.Hausdorff_dist '' s) '' t) =

The Hausdorff distance is invariant under isometries

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

The Hausdorff distance satisfies the triangular inequality

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

The Hausdorff distance satisfies the triangular inequality

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

The Hausdorff distance between a set and its closure vanish

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

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

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

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

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

The Hausdorff distance between two sets and their closures coincide

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

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

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

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

def metric.thickening {α : Type u} (δ : ) (E : set α) :
set α

The (open) `δ`-thickening `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
• = {x : α |
theorem metric.mem_thickening_iff_inf_edist_lt {α : Type u} {δ : } {s : set α} {x : α} :
x
theorem metric.thickening_eq_preimage_inf_edist {α : Type u} (δ : ) (E : set α) :
= (λ (x : α), ⁻¹'

The (open) thickening equals the preimage of an open interval under `inf_edist`.

theorem metric.is_open_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 `thickening δ E` of a fixed subset `E` is an increasing function of the thickening radius `δ`.

theorem metric.thickening_subset_of_subset {α : Type u} (δ : ) {E₁ E₂ : set α} (h : E₁ E₂) :

The (open) thickening `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 : α) (H : z E),
theorem metric.frontier_thickening_subset {α : Type u} (E : set α) {δ : } :
{x : α |

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

theorem metric.frontier_thickening_disjoint {α : Type u} (A : set α) :
theorem metric.mem_thickening_iff {δ : } {X : Type u} {E : set X} {x : X} :
x (z : X) (H : z E), < δ

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) :
{x} = δ
theorem metric.ball_subset_thickening {X : Type u} {x : X} {E : set X} (hx : x E) (δ : ) :
δ
theorem metric.thickening_eq_bUnion_ball {X : Type u} {δ : } {E : set X} :
= (x : X) (H : x E), δ

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

theorem metric.bounded.thickening {X : Type u} {δ : } {E : set X} (h : metric.bounded E) :
def metric.cthickening {α : Type u} (δ : ) (E : set α) :
set α

The closed `δ`-thickening `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
• = {x : α |
@[simp]
theorem metric.mem_cthickening_iff {α : Type u} {δ : } {s : set α} {x : α} :
x
theorem metric.mem_cthickening_of_edist_le {α : Type u} (x y : α) (δ : ) (E : set α) (h : y E) (h' : ) :
x
theorem metric.mem_cthickening_of_dist_le {α : Type u_1} (x y : α) (δ : ) (E : set α) (h : y E) (h' : δ) :
x
theorem metric.cthickening_eq_preimage_inf_edist {α : Type u} (δ : ) (E : set α) :
= (λ (x : α), ⁻¹'
theorem metric.is_closed_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 `cthickening δ E` of a fixed subset `E` is an increasing function of the thickening radius `δ`.

@[simp]
theorem metric.cthickening_singleton {α : Type u_1} (x : α) {δ : } (hδ : 0 δ) :
{x} =
theorem metric.closed_ball_subset_cthickening_singleton {α : Type u_1} (x : α) (δ : ) :
{x}
theorem metric.cthickening_subset_of_subset {α : Type u} (δ : ) {E₁ E₂ : set α} (h : E₁ E₂) :

The closed thickening `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 α) :
theorem metric.cthickening_subset_thickening' {α : Type u} {δ₁ δ₂ : } (δ₂_pos : 0 < δ₂) (hlt : δ₁ < δ₂) (E : set α) :

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

theorem metric.thickening_subset_cthickening {α : Type u} (δ : ) (E : set α) :

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

theorem metric.thickening_subset_cthickening_of_le {α : Type u} {δ₁ δ₂ : } (hle : δ₁ δ₂) (E : set α) :
theorem metric.bounded.cthickening {α : Type u_1} {δ : } {E : set α} (h : metric.bounded E) :
theorem metric.thickening_subset_interior_cthickening {α : Type u} (δ : ) (E : set α) :
theorem metric.closure_thickening_subset_cthickening {α : Type u} (δ : ) (E : set α) :
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_nhds_set {α : Type u} (E : set α) {δ : } (hδ : 0 < δ) :
theorem metric.cthickening_mem_nhds_set {α : Type u} (E : set α) {δ : } (hδ : 0 < δ) :
@[simp]
theorem metric.thickening_union {α : Type u} (δ : ) (s t : set α) :
(s t) =
@[simp]
theorem metric.cthickening_union {α : Type u} (δ : ) (s t : set α) :
(s t) =
@[simp]
theorem metric.thickening_Union {ι : Sort u_1} {α : Type u} (δ : ) (f : ι set α) :
( (i : ι), f i) = (i : ι), (f i)
theorem metric.ediam_cthickening_le {α : Type u} {s : set α} (ε : nnreal) :
+ 2 * ε
theorem metric.ediam_thickening_le {α : Type u} {s : set α} (ε : nnreal) :
+ 2 * ε
theorem metric.diam_cthickening_le {ε : } {α : Type u_1} (s : set α) (hε : 0 ε) :
+ 2 * ε
theorem metric.diam_thickening_le {ε : } {α : Type u_1} (s : set α) (hε : 0 ε) :
+ 2 * ε
@[simp]
theorem metric.thickening_closure {α : Type u} {δ : } {s : set α} :
(closure s) =
@[simp]
theorem metric.cthickening_closure {α : Type u} {δ : } {s : set α} :
=
theorem disjoint.exists_thickenings {α : Type u} {s t : set α} (hst : t) (hs : is_compact s) (ht : is_closed t) :
(δ : ), 0 < δ t)
theorem disjoint.exists_cthickenings {α : Type u} {s t : set α} (hst : t) (hs : is_compact s) (ht : is_closed t) :
(δ : ), 0 < δ t)
theorem is_compact.exists_cthickening_subset_open {α : Type u} {s t : set α} (hs : is_compact s) (ht : is_open t) (hst : s t) :
(δ : ), 0 < δ t
theorem is_compact.exists_thickening_subset_open {α : Type u} {s t : set α} (hs : is_compact s) (ht : is_open t) (hst : s t) :
(δ : ), 0 < δ t
theorem metric.has_basis_nhds_set_thickening {α : Type u} {K : set α} (hK : is_compact K) :
(nhds_set K).has_basis (λ (δ : ), 0 < δ) (λ (δ : ),
theorem metric.has_basis_nhds_set_cthickening {α : Type u} {K : set α} (hK : is_compact K) :
(nhds_set K).has_basis (λ (δ : ), 0 < δ) (λ (δ : ),
theorem metric.cthickening_eq_Inter_cthickening' {α : Type u} {δ : } (s : set ) (hsδ : s ) (hs : (ε : ), δ < ε (s ε).nonempty) (E : set α) :
= (ε : ) (H : ε s),
theorem metric.cthickening_eq_Inter_cthickening {α : Type u} {δ : } (E : set α) :
= (ε : ) (h : δ < ε),
theorem metric.cthickening_eq_Inter_thickening' {α : Type u} {δ : } (δ_nn : 0 δ) (s : set ) (hsδ : s ) (hs : (ε : ), δ < ε (s ε).nonempty) (E : set α) :
= (ε : ) (H : ε s),
theorem metric.cthickening_eq_Inter_thickening {α : Type u} {δ : } (δ_nn : 0 δ) (E : set α) :
= (ε : ) (h : δ < ε),
theorem metric.cthickening_eq_Inter_thickening'' {α : Type u} (δ : ) (E : set α) :
= (ε : ) (h : < ε),
theorem metric.closure_eq_Inter_cthickening' {α : Type u} (E : set α) (s : set ) (hs : (ε : ), 0 < ε (s ε).nonempty) :
= (δ : ) (H : δ s),

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

theorem metric.closure_eq_Inter_cthickening {α : Type u} (E : set α) :
= (δ : ) (h : 0 < δ),

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

theorem metric.closure_eq_Inter_thickening' {α : Type u} (E : set α) (s : set ) (hs₀ : s ) (hs : (ε : ), 0 < ε (s ε).nonempty) :
= (δ : ) (H : δ s),

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

theorem metric.closure_eq_Inter_thickening {α : Type u} (E : set α) :
= (δ : ) (h : 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 `inf_edist` level set.

theorem metric.closed_ball_subset_cthickening {α : Type u_1} {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_Union_closed_ball_of_lt {α : Type u_1} (E : set α) {δ δ' : } (hδ₀ : 0 < δ') (hδδ' : δ < δ') :
(x : α) (H : x E),
theorem is_compact.cthickening_eq_bUnion_closed_ball {α : Type u_1} {δ : } {E : set α} (hE : is_compact E) (hδ : 0 δ) :
= (x : α) (H : x E),

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

See also `metric.cthickening_eq_bUnion_closed_ball`.

theorem metric.cthickening_eq_bUnion_closed_ball {δ : } {α : Type u_1} [proper_space α] (E : set α) (hδ : 0 δ) :
= (x : α) (H : x closure E),
theorem is_closed.cthickening_eq_bUnion_closed_ball {δ : } {α : Type u_1} [proper_space α] {E : set α} (hE : is_closed E) (hδ : 0 δ) :
= (x : α) (H : x E),
theorem metric.inf_edist_le_inf_edist_cthickening_add {α : Type u} {δ : } {s : set α} {x : α} :

For the equality, see `inf_edist_cthickening`.

theorem metric.inf_edist_le_inf_edist_thickening_add {α : Type u} {δ : } {s : set α} {x : α} :

For the equality, see `inf_edist_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 α) :