mathlib3 documentation

topology.metric_space.hausdorff_distance

Hausdorff distance #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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∞. #

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

The minimal edistance of a point to a set

Equations
source
@[simp]
theorem emetric.inf_edist_empty {α : Type u} [pseudo_emetric_space α] {x : α} :
emetric.inf_edist x ∅ = ⊤
source
theorem emetric.le_inf_edist {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} {d : ennreal} :
d ≤ emetric.inf_edist x s ↔ ∀ (y : α), y ∈ s → d ≤ has_edist.edist x y
source
@[simp]
theorem emetric.inf_edist_union {α : Type u} [pseudo_emetric_space α] {x : α} {s t : set α} :
emetric.inf_edist x (s ∪ t) = emetric.inf_edist x s ⊓ emetric.inf_edist x t

The edist to a union is the minimum of the edists

source
@[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)
source
@[simp]
theorem emetric.inf_edist_singleton {α : Type u} [pseudo_emetric_space α] {x y : α} :
emetric.inf_edist x {y} = has_edist.edist x y

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

source
theorem emetric.inf_edist_le_edist_of_mem {α : Type u} [pseudo_emetric_space α] {x y : α} {s : set α} (h : y ∈ s) :
emetric.inf_edist x s ≤ has_edist.edist x y

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

source
theorem emetric.inf_edist_zero_of_mem {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} (h : x ∈ s) :
emetric.inf_edist x s = 0

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

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

The edist is antitone with respect to inclusion.

source
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

source
theorem emetric.inf_edist_le_inf_edist_add_edist {α : Type u} [pseudo_emetric_space α] {x y : α} {s : set α} :
emetric.inf_edist x s ≤ emetric.inf_edist y s + has_edist.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

source
theorem emetric.inf_edist_le_edist_add_inf_edist {α : Type u} [pseudo_emetric_space α] {x y : α} {s : set α} :
emetric.inf_edist x s ≤ has_edist.edist x y + emetric.inf_edist y s
source
theorem emetric.edist_le_inf_edist_add_ediam {α : Type u} [pseudo_emetric_space α] {x y : α} {s : set α} (hy : y ∈ s) :
has_edist.edist x y ≤ emetric.inf_edist x s + emetric.diam s
source
@[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

source
theorem emetric.inf_edist_closure {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} :
emetric.inf_edist x (closure s) = emetric.inf_edist x s

The edist to a set and to its closure coincide

source
theorem emetric.mem_closure_iff_inf_edist_zero {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} :
x ∈ closure s ↔ emetric.inf_edist x s = 0

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

source
theorem emetric.mem_iff_inf_edist_zero_of_closed {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} (h : is_closed s) :
x ∈ s ↔ emetric.inf_edist x s = 0

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

source
theorem emetric.inf_edist_pos_iff_not_mem_closure {α : Type u} [pseudo_emetric_space α] {x : α} {E : set α} :
0 < emetric.inf_edist 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.

source
theorem emetric.inf_edist_closure_pos_iff_not_mem_closure {α : Type u} [pseudo_emetric_space α] {x : α} {E : set α} :
0 < emetric.inf_edist x (closure E) ↔ x ∉ closure E
source
theorem emetric.exists_real_pos_lt_inf_edist_of_not_mem_closure {α : Type u} [pseudo_emetric_space α] {x : α} {E : set α} (h : x ∉ closure E) :
∃ (ε : ℝ), 0 < ε ∧ ennreal.of_real ε < emetric.inf_edist x E
source
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) :
disjoint (emetric.closed_ball x r) s
source
theorem emetric.inf_edist_image {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {x : α} {t : set α} {Φ : α → β} (hΦ : isometry Φ) :
emetric.inf_edist (Φ x) (Φ '' t) = emetric.inf_edist x t

The infimum edistance is invariant under isometries

source
@[simp]
theorem emetric.inf_edist_smul {α : Type u} [pseudo_emetric_space α] {M : Type u_1} [has_smul M α] [has_isometric_smul M α] (c : M) (x : α) (s : set α) :
emetric.inf_edist (c • x) (c • s) = emetric.inf_edist x s
source
@[simp]
theorem emetric.inf_edist_vadd {α : Type u} [pseudo_emetric_space α] {M : Type u_1} [has_vadd M α] [has_isometric_vadd M α] (c : M) (x : α) (s : set α) :
emetric.inf_edist (c +ᵥ x) (c +ᵥ s) = emetric.inf_edist x s
source
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
source
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
source
theorem emetric.exists_pos_forall_lt_edist {α : Type u} [pseudo_emetric_space α] {s t : set α} (hs : is_compact s) (ht : is_closed t) (hst : disjoint s t) :
∃ (r : nnreal), 0 < r ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < has_edist.edist x y

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

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

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

Equations
source
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
source
@[simp]
theorem emetric.Hausdorff_edist_self {α : Type u} [pseudo_emetric_space α] {s : set α} :
emetric.Hausdorff_edist s s = 0

The Hausdorff edistance of a set to itself vanishes

source
theorem emetric.Hausdorff_edist_comm {α : Type u} [pseudo_emetric_space α] {s t : set α} :
emetric.Hausdorff_edist s t = emetric.Hausdorff_edist t s

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

source
theorem emetric.Hausdorff_edist_le_of_inf_edist {α : Type u} [pseudo_emetric_space α] {s t : set α} {r : ennreal} (H1 : ∀ (x : α), x ∈ s → emetric.inf_edist x t ≤ r) (H2 : ∀ (x : α), x ∈ t → emetric.inf_edist x s ≤ r) :
emetric.Hausdorff_edist s t ≤ r

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

source
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)) :
emetric.Hausdorff_edist s t ≤ r

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

source
theorem emetric.inf_edist_le_Hausdorff_edist_of_mem {α : Type u} [pseudo_emetric_space α] {x : α} {s t : set α} (h : x ∈ s) :
emetric.inf_edist x t ≤ emetric.Hausdorff_edist s t

The distance to a set is controlled by the Hausdorff distance

source
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

source
theorem emetric.inf_edist_le_inf_edist_add_Hausdorff_edist {α : Type u} [pseudo_emetric_space α] {x : α} {s t : set α} :
emetric.inf_edist x t ≤ emetric.inf_edist x s + emetric.Hausdorff_edist s t

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

source
theorem emetric.Hausdorff_edist_image {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {s t : set α} {Φ : α → β} (h : isometry Φ) :
emetric.Hausdorff_edist (Φ '' s) (Φ '' t) = emetric.Hausdorff_edist s t

The Hausdorff edistance is invariant under eisometries

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

The Hausdorff distance is controlled by the diameter of the union

source
theorem emetric.Hausdorff_edist_triangle {α : Type u} [pseudo_emetric_space α] {s t u : set α} :
emetric.Hausdorff_edist s u ≤ emetric.Hausdorff_edist s t + emetric.Hausdorff_edist t u

The Hausdorff distance satisfies the triangular inequality

source
theorem emetric.Hausdorff_edist_zero_iff_closure_eq_closure {α : Type u} [pseudo_emetric_space α] {s t : set α} :
emetric.Hausdorff_edist s t = 0 ↔ closure s = closure t

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

source
@[simp]
theorem emetric.Hausdorff_edist_self_closure {α : Type u} [pseudo_emetric_space α] {s : set α} :
emetric.Hausdorff_edist s (closure s) = 0

The Hausdorff edistance between a set and its closure vanishes

source
@[simp]
theorem emetric.Hausdorff_edist_closure₁ {α : Type u} [pseudo_emetric_space α] {s t : set α} :
emetric.Hausdorff_edist (closure s) t = emetric.Hausdorff_edist s t

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

source
@[simp]
theorem emetric.Hausdorff_edist_closure₂ {α : Type u} [pseudo_emetric_space α] {s t : set α} :
emetric.Hausdorff_edist s (closure t) = emetric.Hausdorff_edist s t

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

source
@[simp]
theorem emetric.Hausdorff_edist_closure {α : Type u} [pseudo_emetric_space α] {s t : set α} :
emetric.Hausdorff_edist (closure s) (closure t) = emetric.Hausdorff_edist s t

The Hausdorff edistance between sets or their closures is the same

source
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) :
emetric.Hausdorff_edist s t = 0 ↔ s = t

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

source
theorem emetric.Hausdorff_edist_empty {α : Type u} [pseudo_emetric_space α] {s : set α} (ne : s.nonempty) :
emetric.Hausdorff_edist s ∅ = ⊤

The Haudorff edistance to the empty set is infinite

source
theorem emetric.nonempty_of_Hausdorff_edist_ne_top {α : Type u} [pseudo_emetric_space α] {s t : set α} (hs : s.nonempty) (fin : emetric.Hausdorff_edist s t ≠ ⊤) :
t.nonempty

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

source
theorem emetric.empty_or_nonempty_of_Hausdorff_edist_ne_top {α : Type u} [pseudo_emetric_space α] {s t : set α} (fin : emetric.Hausdorff_edist s t ≠ ⊤) :
s = ∅ ∧ t = ∅ ∨ s.nonempty ∧ t.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 ℝ. #

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

The minimal distance of a point to a set

Equations
source
theorem metric.inf_dist_eq_infi {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :
metric.inf_dist x s = ⨅ (y : ↥s), has_dist.dist x ↑y
source
theorem metric.inf_dist_nonneg {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :
0 ≤ metric.inf_dist x s

the minimal distance is always nonnegative

source
@[simp]
theorem metric.inf_dist_empty {α : Type u} [pseudo_metric_space α] {x : α} :
metric.inf_dist x ∅ = 0

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

source
theorem metric.inf_edist_ne_top {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} (h : s.nonempty) :
emetric.inf_edist x s ≠ ⊤

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

source
theorem metric.inf_dist_zero_of_mem {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} (h : x ∈ s) :
metric.inf_dist x s = 0

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

source
@[simp]
theorem metric.inf_dist_singleton {α : Type u} [pseudo_metric_space α] {x y : α} :
metric.inf_dist x {y} = has_dist.dist x y

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

source
theorem metric.inf_dist_le_dist_of_mem {α : Type u} [pseudo_metric_space α] {s : set α} {x y : α} (h : y ∈ s) :
metric.inf_dist x s ≤ has_dist.dist x y

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

source
theorem metric.inf_dist_le_inf_dist_of_subset {α : Type u} [pseudo_metric_space α] {s t : set α} {x : α} (h : s ⊆ t) (hs : s.nonempty) :
metric.inf_dist x t ≤ metric.inf_dist x s

The minimal distance is monotonous with respect to inclusion

source
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

source
theorem metric.inf_dist_le_inf_dist_add_dist {α : Type u} [pseudo_metric_space α] {s : set α} {x y : α} :
metric.inf_dist x s ≤ metric.inf_dist y s + has_dist.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

source
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
source
theorem metric.disjoint_ball_inf_dist {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :
disjoint (metric.ball x (metric.inf_dist x s)) s
source
theorem metric.ball_inf_dist_subset_compl {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :
metric.ball x (metric.inf_dist x s) ⊆ sᶜ
source
theorem metric.ball_inf_dist_compl_subset {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :
metric.ball x (metric.inf_dist x sᶜ) ⊆ s
source
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) :
disjoint (metric.closed_ball x r) s
source
theorem metric.dist_le_inf_dist_add_diam {α : Type u} [pseudo_metric_space α] {s : set α} {x y : α} (hs : metric.bounded s) (hy : y ∈ s) :
has_dist.dist x y ≤ metric.inf_dist x s + metric.diam s
source
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

source
theorem metric.uniform_continuous_inf_dist_pt {α : Type u} [pseudo_metric_space α] (s : set α) :
uniform_continuous (λ (x : α), metric.inf_dist x s)

The minimal distance to a set is uniformly continuous in point

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

source
theorem metric.inf_dist_eq_closure {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :
metric.inf_dist x (closure s) = metric.inf_dist x s

The minimal distance to a set and its closure coincide

source
theorem metric.inf_dist_zero_of_mem_closure {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} (hx : x ∈ closure s) :
metric.inf_dist 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 mem_closure_iff_inf_dist_zero.

source
theorem metric.mem_closure_iff_inf_dist_zero {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} (h : s.nonempty) :
x ∈ closure s ↔ metric.inf_dist x s = 0

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

source
theorem is_closed.mem_iff_inf_dist_zero {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} (h : is_closed s) (hs : s.nonempty) :
x ∈ s ↔ metric.inf_dist x s = 0

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

source
theorem is_closed.not_mem_iff_inf_dist_pos {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} (h : is_closed s) (hs : s.nonempty) :
x ∉ s ↔ 0 < metric.inf_dist x s

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

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

The infimum distance is invariant under isometries

source
theorem metric.inf_dist_inter_closed_ball_of_mem {α : Type u} [pseudo_metric_space α] {s : set α} {x y : α} (h : y ∈ s) :
metric.inf_dist x (s ∩ metric.closed_ball x (has_dist.dist y x)) = metric.inf_dist x s
source
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
source
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
source
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. #

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

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

Equations
source
@[simp]
theorem metric.coe_inf_nndist {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} :
↑(metric.inf_nndist x s) = metric.inf_dist x s
source
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

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

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

source
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 ℝ. #

source
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
source
theorem metric.Hausdorff_dist_nonneg {α : Type u} [pseudo_metric_space α] {s t : set α} :
0 ≤ metric.Hausdorff_dist s t

The Hausdorff distance is nonnegative

source
theorem metric.Hausdorff_edist_ne_top_of_nonempty_of_bounded {α : Type u} [pseudo_metric_space α] {s t : set α} (hs : s.nonempty) (ht : t.nonempty) (bs : metric.bounded s) (bt : metric.bounded t) :
emetric.Hausdorff_edist s t ≠ ⊤

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

source
@[simp]
theorem metric.Hausdorff_dist_self_zero {α : Type u} [pseudo_metric_space α] {s : set α} :
metric.Hausdorff_dist s s = 0

The Hausdorff distance between a set and itself is zero

source
theorem metric.Hausdorff_dist_comm {α : Type u} [pseudo_metric_space α] {s t : set α} :
metric.Hausdorff_dist s t = metric.Hausdorff_dist t s

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

source
@[simp]
theorem metric.Hausdorff_dist_empty {α : Type u} [pseudo_metric_space α] {s : set α} :
metric.Hausdorff_dist s ∅ = 0

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

source
@[simp]
theorem metric.Hausdorff_dist_empty' {α : Type u} [pseudo_metric_space α] {s : set α} :
metric.Hausdorff_dist ∅ s = 0

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

source
theorem metric.Hausdorff_dist_le_of_inf_dist {α : Type u} [pseudo_metric_space α] {s t : set α} {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ (x : α), x ∈ s → metric.inf_dist x t ≤ r) (H2 : ∀ (x : α), x ∈ t → metric.inf_dist x s ≤ r) :
metric.Hausdorff_dist s t ≤ r

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

source
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)) :
metric.Hausdorff_dist s t ≤ r

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

source
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) :
metric.Hausdorff_dist s t ≤ metric.diam (s ∪ t)

The Hausdorff distance is controlled by the diameter of the union

source
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 ≠ ⊤) :
metric.inf_dist x t ≤ metric.Hausdorff_dist s t

The distance to a set is controlled by the Hausdorff distance

source
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

source
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

source
theorem metric.inf_dist_le_inf_dist_add_Hausdorff_dist {α : Type u} [pseudo_metric_space α] {s t : set α} {x : α} (fin : emetric.Hausdorff_edist s t ≠ ⊤) :
metric.inf_dist x t ≤ metric.inf_dist x s + metric.Hausdorff_dist s t

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

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

The Hausdorff distance is invariant under isometries

source
theorem metric.Hausdorff_dist_triangle {α : Type u} [pseudo_metric_space α] {s t u : set α} (fin : emetric.Hausdorff_edist s t ≠ ⊤) :
metric.Hausdorff_dist s u ≤ metric.Hausdorff_dist s t + metric.Hausdorff_dist t u

The Hausdorff distance satisfies the triangular inequality

source
theorem metric.Hausdorff_dist_triangle' {α : Type u} [pseudo_metric_space α] {s t u : set α} (fin : emetric.Hausdorff_edist t u ≠ ⊤) :
metric.Hausdorff_dist s u ≤ metric.Hausdorff_dist s t + metric.Hausdorff_dist t u

The Hausdorff distance satisfies the triangular inequality

source
@[simp]
theorem metric.Hausdorff_dist_self_closure {α : Type u} [pseudo_metric_space α] {s : set α} :
metric.Hausdorff_dist s (closure s) = 0

The Hausdorff distance between a set and its closure vanish

source
@[simp]
theorem metric.Hausdorff_dist_closure₁ {α : Type u} [pseudo_metric_space α] {s t : set α} :
metric.Hausdorff_dist (closure s) t = metric.Hausdorff_dist s t

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

source
@[simp]
theorem metric.Hausdorff_dist_closure₂ {α : Type u} [pseudo_metric_space α] {s t : set α} :
metric.Hausdorff_dist s (closure t) = metric.Hausdorff_dist s t

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

source
@[simp]
theorem metric.Hausdorff_dist_closure {α : Type u} [pseudo_metric_space α] {s t : set α} :
metric.Hausdorff_dist (closure s) (closure t) = metric.Hausdorff_dist s t

The Hausdorff distance between two sets and their closures coincide

source
theorem metric.Hausdorff_dist_zero_iff_closure_eq_closure {α : Type u} [pseudo_metric_space α] {s t : set α} (fin : emetric.Hausdorff_edist s t ≠ ⊤) :
metric.Hausdorff_dist s t = 0 ↔ closure s = closure t

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

source
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 ≠ ⊤) :
metric.Hausdorff_dist s t = 0 ↔ s = t

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

source
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
source
theorem metric.mem_thickening_iff_inf_edist_lt {α : Type u} [pseudo_emetric_space α] {δ : ℝ} {s : set α} {x : α} :
x ∈ metric.thickening δ s ↔ emetric.inf_edist x s < ennreal.of_real δ
source
theorem metric.thickening_eq_preimage_inf_edist {α : Type u} [pseudo_emetric_space α] (δ : ℝ) (E : set α) :
metric.thickening δ E = (λ (x : α), emetric.inf_edist x E) ⁻¹' set.Iio (ennreal.of_real δ)

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

source
theorem metric.is_open_thickening {α : Type u} [pseudo_emetric_space α] {δ : ℝ} {E : set α} :
is_open (metric.thickening δ E)

The (open) thickening is an open set.

source
@[simp]
theorem metric.thickening_empty {α : Type u} [pseudo_emetric_space α] (δ : ℝ) :
metric.thickening δ ∅ = ∅

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

source
theorem metric.thickening_of_nonpos {α : Type u} [pseudo_emetric_space α] {δ : ℝ} (hδ : δ ≤ 0) (s : set α) :
metric.thickening δ s = ∅
source
theorem metric.thickening_mono {α : Type u} [pseudo_emetric_space α] {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : set α) :
metric.thickening δ₁ E ⊆ metric.thickening δ₂ E

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

source
theorem metric.thickening_subset_of_subset {α : Type u} [pseudo_emetric_space α] (δ : ℝ) {E₁ E₂ : set α} (h : E₁ ⊆ E₂) :
metric.thickening δ E₁ ⊆ metric.thickening δ E₂

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

source
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 δ
source
theorem metric.frontier_thickening_subset {α : Type u} [pseudo_emetric_space α] (E : set α) {δ : ℝ} :
frontier (metric.thickening δ E) ⊆ {x : α | emetric.inf_edist x E = ennreal.of_real δ}

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

source
theorem metric.frontier_thickening_disjoint {α : Type u} [pseudo_emetric_space α] (A : set α) :
pairwise (disjoint on λ (r : ℝ), frontier (metric.thickening r A))
source
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.

source
@[simp]
theorem metric.thickening_singleton {X : Type u} [pseudo_metric_space X] (δ : ℝ) (x : X) :
metric.thickening δ {x} = metric.ball x δ
source
theorem metric.ball_subset_thickening {X : Type u} [pseudo_metric_space X] {x : X} {E : set X} (hx : x ∈ E) (δ : ℝ) :
metric.ball x δ ⊆ metric.thickening δ E
source
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.

source
theorem metric.bounded.thickening {X : Type u} [pseudo_metric_space X] {δ : ℝ} {E : set X} (h : metric.bounded E) :
metric.bounded (metric.thickening δ E)
source
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
source
@[simp]
theorem metric.mem_cthickening_iff {α : Type u} [pseudo_emetric_space α] {δ : ℝ} {s : set α} {x : α} :
x ∈ metric.cthickening δ s ↔ emetric.inf_edist x s ≤ ennreal.of_real δ
source
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 δ) :
x ∈ metric.cthickening δ E
source
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 ≤ δ) :
x ∈ metric.cthickening δ E
source
theorem metric.cthickening_eq_preimage_inf_edist {α : Type u} [pseudo_emetric_space α] (δ : ℝ) (E : set α) :
metric.cthickening δ E = (λ (x : α), emetric.inf_edist x E) ⁻¹' set.Iic (ennreal.of_real δ)
source
theorem metric.is_closed_cthickening {α : Type u} [pseudo_emetric_space α] {δ : ℝ} {E : set α} :
is_closed (metric.cthickening δ E)

The closed thickening is a closed set.

source
@[simp]
theorem metric.cthickening_empty {α : Type u} [pseudo_emetric_space α] (δ : ℝ) :
metric.cthickening δ ∅ = ∅

The closed thickening of the empty set is empty.

source
theorem metric.cthickening_of_nonpos {α : Type u} [pseudo_emetric_space α] {δ : ℝ} (hδ : δ ≤ 0) (E : set α) :
metric.cthickening δ E = closure E
source
@[simp]
theorem metric.cthickening_zero {α : Type u} [pseudo_emetric_space α] (E : set α) :
metric.cthickening 0 E = closure E

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

source
theorem metric.cthickening_max_zero {α : Type u} [pseudo_emetric_space α] (δ : ℝ) (E : set α) :
metric.cthickening (linear_order.max 0 δ) E = metric.cthickening δ E
source
theorem metric.cthickening_mono {α : Type u} [pseudo_emetric_space α] {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : set α) :
metric.cthickening δ₁ E ⊆ metric.cthickening δ₂ E

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

source
@[simp]
theorem metric.cthickening_singleton {α : Type u_1} [pseudo_metric_space α] (x : α) {δ : ℝ} (hδ : 0 ≤ δ) :
metric.cthickening δ {x} = metric.closed_ball x δ
source
theorem metric.closed_ball_subset_cthickening_singleton {α : Type u_1} [pseudo_metric_space α] (x : α) (δ : ℝ) :
metric.closed_ball x δ ⊆ metric.cthickening δ {x}
source
theorem metric.cthickening_subset_of_subset {α : Type u} [pseudo_emetric_space α] (δ : ℝ) {E₁ E₂ : set α} (h : E₁ ⊆ E₂) :
metric.cthickening δ E₁ ⊆ metric.cthickening δ E₂

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

source
theorem metric.cthickening_subset_thickening {α : Type u} [pseudo_emetric_space α] {δ₁ : nnreal} {δ₂ : ℝ} (hlt : ↑δ₁ < δ₂) (E : set α) :
metric.cthickening ↑δ₁ E ⊆ metric.thickening δ₂ E
source
theorem metric.cthickening_subset_thickening' {α : Type u} [pseudo_emetric_space α] {δ₁ δ₂ : ℝ} (δ₂_pos : 0 < δ₂) (hlt : δ₁ < δ₂) (E : set α) :
metric.cthickening δ₁ E ⊆ metric.thickening δ₂ E

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

source
theorem metric.thickening_subset_cthickening {α : Type u} [pseudo_emetric_space α] (δ : ℝ) (E : set α) :
metric.thickening δ E ⊆ metric.cthickening δ E

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

source
theorem metric.thickening_subset_cthickening_of_le {α : Type u} [pseudo_emetric_space α] {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : set α) :
metric.thickening δ₁ E ⊆ metric.cthickening δ₂ E
source
theorem metric.bounded.cthickening {α : Type u_1} [pseudo_metric_space α] {δ : ℝ} {E : set α} (h : metric.bounded E) :
metric.bounded (metric.cthickening δ E)
source
theorem metric.thickening_subset_interior_cthickening {α : Type u} [pseudo_emetric_space α] (δ : ℝ) (E : set α) :
metric.thickening δ E ⊆ interior (metric.cthickening δ E)
source
theorem metric.closure_thickening_subset_cthickening {α : Type u} [pseudo_emetric_space α] (δ : ℝ) (E : set α) :
closure (metric.thickening δ E) ⊆ metric.cthickening δ E
source
theorem metric.closure_subset_cthickening {α : Type u} [pseudo_emetric_space α] (δ : ℝ) (E : set α) :
closure E ⊆ metric.cthickening δ E

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

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

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

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

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

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

A set is contained in its own closed thickening.

source
theorem metric.thickening_mem_nhds_set {α : Type u} [pseudo_emetric_space α] (E : set α) {δ : ℝ} (hδ : 0 < δ) :
metric.thickening δ E ∈ nhds_set E
source
theorem metric.cthickening_mem_nhds_set {α : Type u} [pseudo_emetric_space α] (E : set α) {δ : ℝ} (hδ : 0 < δ) :
metric.cthickening δ E ∈ nhds_set E
source
@[simp]
theorem metric.thickening_union {α : Type u} [pseudo_emetric_space α] (δ : ℝ) (s t : set α) :
metric.thickening δ (s ∪ t) = metric.thickening δ s ∪ metric.thickening δ t
source
@[simp]
theorem metric.cthickening_union {α : Type u} [pseudo_emetric_space α] (δ : ℝ) (s t : set α) :
metric.cthickening δ (s ∪ t) = metric.cthickening δ s ∪ metric.cthickening δ t
source
@[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)
source
theorem metric.ediam_cthickening_le {α : Type u} [pseudo_emetric_space α] {s : set α} (ε : nnreal) :
emetric.diam (metric.cthickening ↑ε s) ≤ emetric.diam s + 2 * ↑ε
source
theorem metric.ediam_thickening_le {α : Type u} [pseudo_emetric_space α] {s : set α} (ε : nnreal) :
emetric.diam (metric.thickening ↑ε s) ≤ emetric.diam s + 2 * ↑ε
source
theorem metric.diam_cthickening_le {ε : ℝ} {α : Type u_1} [pseudo_metric_space α] (s : set α) (hε : 0 ≤ ε) :
metric.diam (metric.cthickening ε s) ≤ metric.diam s + 2 * ε
source
theorem metric.diam_thickening_le {ε : ℝ} {α : Type u_1} [pseudo_metric_space α] (s : set α) (hε : 0 ≤ ε) :
metric.diam (metric.thickening ε s) ≤ metric.diam s + 2 * ε
source
@[simp]
theorem metric.thickening_closure {α : Type u} [pseudo_emetric_space α] {δ : ℝ} {s : set α} :
metric.thickening δ (closure s) = metric.thickening δ s
source
@[simp]
theorem metric.cthickening_closure {α : Type u} [pseudo_emetric_space α] {δ : ℝ} {s : set α} :
metric.cthickening δ (closure s) = metric.cthickening δ s
source
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)
source
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)
source
theorem is_compact.exists_cthickening_subset_open {α : Type u} [pseudo_emetric_space α] {s t : set α} (hs : is_compact s) (ht : is_open t) (hst : s ⊆ t) :
∃ (δ : ℝ), 0 < δ ∧ metric.cthickening δ s ⊆ t
source
theorem is_compact.exists_thickening_subset_open {α : Type u} [pseudo_emetric_space α] {s t : set α} (hs : is_compact s) (ht : is_open t) (hst : s ⊆ t) :
∃ (δ : ℝ), 0 < δ ∧ metric.thickening δ s ⊆ t
source
theorem metric.has_basis_nhds_set_thickening {α : Type u} [pseudo_emetric_space α] {K : set α} (hK : is_compact K) :
(nhds_set K).has_basis (λ (δ : ℝ), 0 < δ) (λ (δ : ℝ), metric.thickening δ K)
source
theorem metric.has_basis_nhds_set_cthickening {α : Type u} [pseudo_emetric_space α] {K : set α} (hK : is_compact K) :
(nhds_set K).has_basis (λ (δ : ℝ), 0 < δ) (λ (δ : ℝ), metric.cthickening δ K)
source
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
source
theorem metric.cthickening_eq_Inter_cthickening {α : Type u} [pseudo_emetric_space α] {δ : ℝ} (E : set α) :
metric.cthickening δ E = ⋂ (ε : ℝ) (h : δ < ε), metric.cthickening ε E
source
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
source
theorem metric.cthickening_eq_Inter_thickening {α : Type u} [pseudo_emetric_space α] {δ : ℝ} (δ_nn : 0 ≤ δ) (E : set α) :
metric.cthickening δ E = ⋂ (ε : ℝ) (h : δ < ε), metric.thickening ε E
source
theorem metric.cthickening_eq_Inter_thickening'' {α : Type u} [pseudo_emetric_space α] (δ : ℝ) (E : set α) :
metric.cthickening δ E = ⋂ (ε : ℝ) (h : linear_order.max 0 δ < ε), metric.thickening ε E
source
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.

source
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.

source
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.

source
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.

source
theorem metric.frontier_cthickening_subset {α : Type u} [pseudo_emetric_space α] (E : set α) {δ : ℝ} :
frontier (metric.cthickening δ E) ⊆ {x : α | emetric.inf_edist x E = ennreal.of_real δ}

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

source
theorem metric.closed_ball_subset_cthickening {α : Type u_1} [pseudo_metric_space α] {x : α} {E : set α} (hx : x ∈ E) (δ : ℝ) :
metric.closed_ball x δ ⊆ metric.cthickening δ E

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

source
theorem metric.cthickening_subset_Union_closed_ball_of_lt {α : Type u_1} [pseudo_metric_space α] (E : set α) {δ δ' : ℝ} (hδ₀ : 0 < δ') (hδδ' : δ < δ') :
metric.cthickening δ E ⊆ ⋃ (x : α) (H : x ∈ E), metric.closed_ball x δ'
source
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.

See also metric.cthickening_eq_bUnion_closed_ball.

source
theorem metric.cthickening_eq_bUnion_closed_ball {δ : ℝ} {α : Type u_1} [pseudo_metric_space α] [proper_space α] (E : set α) (hδ : 0 ≤ δ) :
metric.cthickening δ E = ⋃ (x : α) (H : x ∈ closure E), metric.closed_ball x δ
source
theorem is_closed.cthickening_eq_bUnion_closed_ball {δ : ℝ} {α : Type u_1} [pseudo_metric_space α] [proper_space α] {E : set α} (hE : is_closed E) (hδ : 0 ≤ δ) :
metric.cthickening δ E = ⋃ (x : α) (H : x ∈ E), metric.closed_ball x δ
source
theorem metric.inf_edist_le_inf_edist_cthickening_add {α : Type u} [pseudo_emetric_space α] {δ : ℝ} {s : set α} {x : α} :
emetric.inf_edist x s ≤ emetric.inf_edist x (metric.cthickening δ s) + ennreal.of_real δ

For the equality, see inf_edist_cthickening.

source
theorem metric.inf_edist_le_inf_edist_thickening_add {α : Type u} [pseudo_emetric_space α] {δ : ℝ} {s : set α} {x : α} :
emetric.inf_edist x s ≤ emetric.inf_edist x (metric.thickening δ s) + ennreal.of_real δ

For the equality, see inf_edist_thickening.

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

For the equality, see thickening_thickening.

source
@[simp]
theorem metric.thickening_cthickening_subset {α : Type u} [pseudo_emetric_space α] {δ : ℝ} (ε : ℝ) (hδ : 0 ≤ δ) (s : set α) :
metric.thickening ε (metric.cthickening δ s) ⊆ metric.thickening (ε + δ) s

For the equality, see thickening_cthickening.

source
@[simp]
theorem metric.cthickening_thickening_subset {α : Type u} [pseudo_emetric_space α] {ε : ℝ} (hε : 0 ≤ ε) (δ : ℝ) (s : set α) :
metric.cthickening ε (metric.thickening δ s) ⊆ metric.cthickening (ε + δ) s

For the equality, see cthickening_thickening.

source
@[simp]
theorem metric.cthickening_cthickening_subset {α : Type u} [pseudo_emetric_space α] {δ ε : ℝ} (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (s : set α) :
metric.cthickening ε (metric.cthickening δ s) ⊆ metric.cthickening (ε + δ) s

For the equality, see cthickening_cthickening.

source
theorem metric.frontier_cthickening_disjoint {α : Type u} [pseudo_emetric_space α] (A : set α) :
pairwise (disjoint on λ (r : nnreal), frontier (metric.cthickening ↑r A))