mathlib documentation

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:

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

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

The minimal edistance of a point to a set

Equations
@[simp]
theorem emetric.inf_edist_empty {α : Type u} [pseudo_emetric_space α] {x : α} :
theorem emetric.le_inf_edist {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} {d : ennreal} :
d emetric.inf_edist x s ∀ (y : α), y sd has_edist.edist x y
@[simp]
theorem emetric.inf_edist_union {α : Type u} [pseudo_emetric_space α] {x : α} {s t : set α} :

The edist to a union is the minimum of the edists

@[simp]
theorem emetric.inf_edist_Union {ι : Sort u_1} {α : Type u} [pseudo_emetric_space α] (f : ι → set α) (x : α) :
emetric.inf_edist x (⋃ (i : ι), f i) = ⨅ (i : ι), emetric.inf_edist x (f i)
@[simp]
theorem emetric.inf_edist_singleton {α : Type u} [pseudo_emetric_space α] {x 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} [pseudo_emetric_space α] {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} [pseudo_emetric_space α] {x : α} {s : set α} (h : x s) :

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

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

The edist is antitone with respect to inclusion.

theorem emetric.inf_edist_lt_iff {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} {r : ennreal} :
emetric.inf_edist x s < r ∃ (y : α) (H : y s), has_edist.edist x y < r

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

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

@[continuity]
theorem emetric.continuous_inf_edist {α : Type u} [pseudo_emetric_space α] {s : set α} :
continuous (λ (x : α), emetric.inf_edist x s)

The edist to a set depends continuously on the point

theorem emetric.inf_edist_closure {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} :

The edist to a set and to its closure coincide

theorem emetric.mem_closure_iff_inf_edist_zero {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} :

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} [pseudo_emetric_space α] {x : α} {s : set α} (h : is_closed s) :

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

theorem emetric.disjoint_closed_ball_of_lt_inf_edist {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} {r : ennreal} (h : r < emetric.inf_edist x s) :
theorem emetric.inf_edist_image {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {x : α} {t : set α} {Φ : α → β} (hΦ : isometry Φ) :

The infimum edistance is invariant under isometries

theorem is_open.exists_Union_is_closed {α : Type u} [pseudo_emetric_space α] {U : set α} (hU : is_open U) :
∃ (F : set α), (∀ (n : ), is_closed (F n)) (∀ (n : ), F n U) (⋃ (n : ), F n) = U monotone F
theorem is_compact.exists_inf_edist_eq_edist {α : Type u} [pseudo_emetric_space α] {s : set α} (hs : is_compact s) (hne : s.nonempty) (x : α) :
∃ (y : α) (H : y s), emetric.inf_edist x s = has_edist.edist x y
theorem emetric.exists_pos_forall_le_edist {α : Type u} [pseudo_emetric_space α] {s t : set α} (hs : is_compact s) (hs' : s.nonempty) (ht : is_closed t) (hst : disjoint s t) :
∃ (r : ennreal), 0 < r ∀ (x : α), x s∀ (y : α), y tr has_edist.edist x y

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

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

The Hausdorff edistance of a set to itself vanishes

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

theorem emetric.Hausdorff_edist_le_of_inf_edist {α : Type u} [pseudo_emetric_space α] {s t : set α} {r : ennreal} (H1 : ∀ (x : α), x semetric.inf_edist x t r) (H2 : ∀ (x : α), x temetric.inf_edist x s 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} [pseudo_emetric_space α] {s t : set α} {r : ennreal} (H1 : ∀ (x : α), x s(∃ (y : α) (H : y t), has_edist.edist x y r)) (H2 : ∀ (x : α), x t(∃ (y : α) (H : y s), has_edist.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.inf_edist_le_Hausdorff_edist_of_mem {α : Type u} [pseudo_emetric_space α] {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} [pseudo_emetric_space α] {x : α} {s t : set α} {r : ennreal} (h : x s) (H : emetric.Hausdorff_edist s t < r) :
∃ (y : α) (H : y t), has_edist.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

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} [pseudo_emetric_space α] [pseudo_emetric_space β] {s t : set α} {Φ : α → β} (h : isometry Φ) :

The Hausdorff edistance is invariant under eisometries

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

The Hausdorff distance is controlled by the diameter of the union

The Hausdorff distance satisfies the triangular inequality

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

@[simp]

The Hausdorff edistance between a set and its closure vanishes

@[simp]

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

@[simp]

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

@[simp]

The Hausdorff edistance between sets or their closures is the same

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

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

The Haudorff edistance to the empty set is infinite

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

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} [pseudo_metric_space α] (x : α) (s : set α) :

The minimal distance of a point to a set

Equations
theorem metric.inf_dist_nonneg {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :

the minimal distance is always nonnegative

@[simp]
theorem metric.inf_dist_empty {α : Type u} [pseudo_metric_space α] {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} [pseudo_metric_space α] {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} [pseudo_metric_space α] {s : set α} {x : α} (h : x s) :

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

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

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

theorem metric.inf_dist_le_dist_of_mem {α : Type u} [pseudo_metric_space α] {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} [pseudo_metric_space α] {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} [pseudo_metric_space α] {s : set α} {x : α} {r : } (hs : s.nonempty) :
metric.inf_dist x s < r ∃ (y : α) (H : y s), has_dist.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.inf_dist_le_inf_dist_add_dist {α : Type u} [pseudo_metric_space α] {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} [pseudo_metric_space α] {s : set α} {x y : α} (h : has_dist.dist x y < metric.inf_dist x s) :
y s
theorem metric.disjoint_ball_inf_dist {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :
theorem metric.ball_inf_dist_subset_compl {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :
theorem metric.ball_inf_dist_compl_subset {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :
theorem metric.disjoint_closed_ball_of_lt_inf_dist {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} {r : } (h : r < metric.inf_dist x s) :
theorem metric.lipschitz_inf_dist_pt {α : Type u} [pseudo_metric_space α] (s : set α) :
lipschitz_with 1 (λ (x : α), metric.inf_dist x s)

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

theorem metric.uniform_continuous_inf_dist_pt {α : Type u} [pseudo_metric_space α] (s : set α) :

The minimal distance to a set is uniformly continuous in point

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

The minimal distance to a set is continuous in point

theorem metric.inf_dist_eq_closure {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :

The minimal distance to a set and its closure coincide

theorem metric.inf_dist_zero_of_mem_closure {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} (hx : x closure s) :

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} [pseudo_metric_space α] {s : set α} {x : α} (h : s.nonempty) :

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} [pseudo_metric_space α] {s : set α} {x : α} (h : is_closed s) (hs : s.nonempty) :

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} [pseudo_metric_space α] {s : set α} {x : α} (h : is_closed s) (hs : s.nonempty) :

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} [pseudo_metric_space α] [pseudo_metric_space β] {t : set α} {x : α} {Φ : α → β} (hΦ : isometry Φ) :

The infimum distance is invariant under isometries

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

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

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

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

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

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

theorem metric.uniform_continuous_inf_nndist_pt {α : Type u} [pseudo_metric_space α] (s : set α) :

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

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

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} [pseudo_metric_space α] (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} [pseudo_metric_space α] {s t : set α} :

The Hausdorff distance is nonnegative

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} [pseudo_metric_space α] {s : set α} :

The Hausdorff distance between a set and itself is zero

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

@[simp]
theorem metric.Hausdorff_dist_empty {α : Type u} [pseudo_metric_space α] {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} [pseudo_metric_space α] {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} [pseudo_metric_space α] {s t : set α} {r : } (hr : 0 r) (H1 : ∀ (x : α), x smetric.inf_dist x t r) (H2 : ∀ (x : α), x tmetric.inf_dist x s 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} [pseudo_metric_space α] {s t : set α} {r : } (hr : 0 r) (H1 : ∀ (x : α), x s(∃ (y : α) (H : y t), has_dist.dist x y r)) (H2 : ∀ (x : α), x t(∃ (y : α) (H : y s), has_dist.dist x y r)) :

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

theorem metric.Hausdorff_dist_le_diam {α : Type u} [pseudo_metric_space α] {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} [pseudo_metric_space α] {s t : set α} {x : α} (hx : x s) (fin : emetric.Hausdorff_edist s t ) :

The distance to a set is controlled by the Hausdorff distance

theorem metric.exists_dist_lt_of_Hausdorff_dist_lt {α : Type u} [pseudo_metric_space α] {s t : set α} {x : α} {r : } (h : x s) (H : metric.Hausdorff_dist s t < r) (fin : emetric.Hausdorff_edist s t ) :
∃ (y : α) (H : y t), has_dist.dist x y < r

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

theorem metric.exists_dist_lt_of_Hausdorff_dist_lt' {α : Type u} [pseudo_metric_space α] {s t : set α} {y : α} {r : } (h : y t) (H : metric.Hausdorff_dist s t < r) (fin : emetric.Hausdorff_edist s t ) :
∃ (x : α) (H : x s), has_dist.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

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} [pseudo_metric_space α] [pseudo_metric_space β] {s t : set α} {Φ : α → β} (h : isometry Φ) :

The Hausdorff distance is invariant under isometries

The Hausdorff distance satisfies the triangular inequality

The Hausdorff distance satisfies the triangular inequality

@[simp]

The Hausdorff distance between a set and its closure vanish

@[simp]

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

@[simp]

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

@[simp]

The Hausdorff distance between two sets and their closures coincide

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} [pseudo_metric_space α] {s t : set α} (hs : is_closed s) (ht : is_closed t) (fin : emetric.Hausdorff_edist s t ) :

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

def metric.thickening {α : Type u} [pseudo_emetric_space α] (δ : ) (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
theorem metric.thickening_eq_preimage_inf_edist {α : Type u} [pseudo_emetric_space α] (δ : ) (E : set α) :

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

theorem metric.is_open_thickening {α : Type u} [pseudo_emetric_space α] {δ : } {E : set α} :

The (open) thickening is an open set.

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

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

theorem metric.thickening_of_nonpos {α : Type u} [pseudo_emetric_space α] {δ : } (hδ : δ 0) (s : set α) :
theorem metric.thickening_mono {α : Type u} [pseudo_emetric_space α] {δ₁ δ₂ : } (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} [pseudo_emetric_space α] (δ : ) {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} [pseudo_emetric_space α] {δ : } (E : set α) (x : α) :
x metric.thickening δ E ∃ (z : α) (H : z E), has_edist.edist x z < ennreal.of_real δ
theorem metric.mem_thickening_iff {δ : } {X : Type u} [pseudo_metric_space X] {E : set X} {x : X} :
x metric.thickening δ E ∃ (z : X) (H : z E), has_dist.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} [pseudo_metric_space X] (δ : ) (x : X) :
theorem metric.thickening_eq_bUnion_ball {X : Type u} [pseudo_metric_space X] {δ : } {E : set X} :
metric.thickening δ E = ⋃ (x : X) (H : x E), metric.ball x δ

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.

def metric.cthickening {α : Type u} [pseudo_emetric_space α] (δ : ) (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
@[simp]
theorem metric.mem_cthickening_iff {α : Type u} [pseudo_emetric_space α] {δ : } {s : set α} {x : α} :
theorem metric.mem_cthickening_of_edist_le {α : Type u} [pseudo_emetric_space α] (x y : α) (δ : ) (E : set α) (h : y E) (h' : has_edist.edist x y ennreal.of_real δ) :
theorem metric.mem_cthickening_of_dist_le {α : Type u_1} [pseudo_metric_space α] (x y : α) (δ : ) (E : set α) (h : y E) (h' : has_dist.dist x y δ) :
theorem metric.is_closed_cthickening {α : Type u} [pseudo_emetric_space α] {δ : } {E : set α} :

The closed thickening is a closed set.

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

The closed thickening of the empty set is empty.

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

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

theorem metric.cthickening_mono {α : Type u} [pseudo_emetric_space α] {δ₁ δ₂ : } (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} [pseudo_metric_space α] (x : α) {δ : } (hδ : 0 δ) :
theorem metric.cthickening_subset_of_subset {α : Type u} [pseudo_emetric_space α] (δ : ) {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} [pseudo_emetric_space α] {δ₁ : nnreal} {δ₂ : } (hlt : δ₁ < δ₂) (E : set α) :
theorem metric.cthickening_subset_thickening' {α : Type u} [pseudo_emetric_space α] {δ₁ δ₂ : } (δ₂_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.

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} [pseudo_emetric_space α] {δ₁ δ₂ : } (hle : δ₁ δ₂) (E : set α) :
theorem metric.bounded.cthickening {α : Type u_1} [pseudo_metric_space α] {δ : } {E : set α} (h : metric.bounded E) :
theorem metric.closure_subset_cthickening {α : Type u} [pseudo_emetric_space α] (δ : ) (E : set α) :

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

theorem metric.closure_subset_thickening {α : Type u} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) :

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

theorem metric.self_subset_thickening {α : Type u} [pseudo_emetric_space α] {δ : } (δ_pos : 0 < δ) (E : set α) :

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

theorem metric.self_subset_cthickening {α : Type u} [pseudo_emetric_space α] {δ : } (E : set α) :

A set is contained in its own closed thickening.

@[simp]
theorem metric.thickening_union {α : Type u} [pseudo_emetric_space α] (δ : ) (s t : set α) :
@[simp]
theorem metric.cthickening_union {α : Type u} [pseudo_emetric_space α] (δ : ) (s t : set α) :
@[simp]
theorem metric.thickening_Union {ι : Sort u_1} {α : Type u} [pseudo_emetric_space α] (δ : ) (f : ι → set α) :
metric.thickening δ (⋃ (i : ι), f i) = ⋃ (i : ι), metric.thickening δ (f i)
@[simp]
theorem metric.thickening_closure {α : Type u} [pseudo_emetric_space α] {δ : } {s : set α} :
@[simp]
theorem metric.cthickening_closure {α : Type u} [pseudo_emetric_space α] {δ : } {s : set α} :
theorem disjoint.exists_thickenings {α : Type u} [pseudo_emetric_space α] {s t : set α} (hst : disjoint s t) (hs : is_compact s) (ht : is_closed t) :
∃ (δ : ), 0 < δ disjoint (metric.thickening δ s) (metric.thickening δ t)
theorem disjoint.exists_cthickenings {α : Type u} [pseudo_emetric_space α] {s t : set α} (hst : disjoint s t) (hs : is_compact s) (ht : is_closed t) :
∃ (δ : ), 0 < δ disjoint (metric.cthickening δ s) (metric.cthickening δ t)
theorem metric.cthickening_eq_Inter_cthickening' {α : Type u} [pseudo_emetric_space α] {δ : } (s : set ) (hsδ : s set.Ioi δ) (hs : ∀ (ε : ), δ < ε(s set.Ioc δ ε).nonempty) (E : set α) :
metric.cthickening δ E = ⋂ (ε : ) (H : ε s), metric.cthickening ε E
theorem metric.cthickening_eq_Inter_cthickening {α : Type u} [pseudo_emetric_space α] {δ : } (E : set α) :
metric.cthickening δ E = ⋂ (ε : ) (h : δ < ε), metric.cthickening ε E
theorem metric.cthickening_eq_Inter_thickening' {α : Type u} [pseudo_emetric_space α] {δ : } (δ_nn : 0 δ) (s : set ) (hsδ : s set.Ioi δ) (hs : ∀ (ε : ), δ < ε(s set.Ioc δ ε).nonempty) (E : set α) :
metric.cthickening δ E = ⋂ (ε : ) (H : ε s), metric.thickening ε E
theorem metric.cthickening_eq_Inter_thickening {α : Type u} [pseudo_emetric_space α] {δ : } (δ_nn : 0 δ) (E : set α) :
metric.cthickening δ E = ⋂ (ε : ) (h : δ < ε), metric.thickening ε E
theorem metric.closure_eq_Inter_cthickening' {α : Type u} [pseudo_emetric_space α] (E : set α) (s : set ) (hs : ∀ (ε : ), 0 < ε(s set.Ioc 0 ε).nonempty) :
closure E = ⋂ (δ : ) (H : δ 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_Inter_cthickening {α : Type u} [pseudo_emetric_space α] (E : set α) :
closure E = ⋂ (δ : ) (h : 0 < δ), metric.cthickening δ E

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

theorem metric.closure_eq_Inter_thickening' {α : Type u} [pseudo_emetric_space α] (E : set α) (s : set ) (hs₀ : s set.Ioi 0) (hs : ∀ (ε : ), 0 < ε(s set.Ioc 0 ε).nonempty) :
closure E = ⋂ (δ : ) (H : δ 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_Inter_thickening {α : Type u} [pseudo_emetric_space α] (E : set α) :
closure E = ⋂ (δ : ) (h : 0 < δ), metric.thickening δ E

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

theorem metric.frontier_thickening_subset {α : Type u} [pseudo_emetric_space α] (E : set α) {δ : } (δ_pos : 0 < δ) :

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

theorem metric.frontier_cthickening_subset {α : Type u} [pseudo_emetric_space α] (E : set α) {δ : } :

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} [pseudo_metric_space α] {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 is_compact.cthickening_eq_bUnion_closed_ball {α : Type u_1} [pseudo_metric_space α] {δ : } {E : set α} (hE : is_compact E) (hδ : 0 δ) :
metric.cthickening δ E = ⋃ (x : α) (H : x E), metric.closed_ball x δ

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

@[simp]
theorem metric.thickening_thickening_subset {α : Type u} [pseudo_emetric_space α] (ε δ : ) (s : set α) :

For the equality, see thickening_thickening.

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

For the equality, see thickening_cthickening.

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

For the equality, see cthickening_thickening.

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

For the equality, see cthickening_cthickening.