Thickenings in pseudo-metric spaces

Main definitions

• Metric.thickening δ s, the open thickening by radius δ of a set s in a pseudo emetric space.
• Metric.cthickening δ s, the closed thickening by radius δ of a set s in a pseudo emetric space.

Main results

• Disjoint.exists_thickenings: two disjoint sets admit disjoint thickenings

• Disjoint.exists_cthickenings: two disjoint sets admit disjoint closed thickenings

• IsCompact.exists_cthickening_subset_open: if s is compact, t is open and s ⊆ t, some cthickening of s is contained in t.

• Metric.hasBasis_nhdsSet_cthickening: the cthickenings of a compact set K form a basis of the neighbourhoods of K

• Metric.closure_eq_iInter_cthickening': the closure of a set equals the intersection of its closed thickenings of positive radii accumulating at zero. The same holds for open thickenings.

• IsCompact.cthickening_eq_biUnion_closedBall: if s is compact, cthickening δ s is the union of closedBalls of radius δ around x : E.

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

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

Equations

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

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

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

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

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

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

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

The (open) thickening is an open set.

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

Any set is contained in the complement of the δ-thickening of the complement of its δ-thickening.

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

The δ-thickening of the complement of the δ-thickening of a set is contained in the complement of the set.

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

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

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

@[simp]

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

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

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

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

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

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

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

Equations

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

@[simp]

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

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

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

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

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

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

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

The closed thickening is a closed set.

@[simp]

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

The closed thickening of the empty set is empty.

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

A set is contained in its own closed thickening.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Metric.thickening_biUnion {α : Type u} [PseudoEMetricSpace α] {ι : Type u_2} (δ : ℝ) (f : ι → Set α) (I : Set ι) : Metric.thickening δ (⋃ i ∈ I, f i) = ⋃ i ∈ I, Metric.thickening δ (f i)

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

If s is compact, t is open and s ⊆ t, some cthickening of s is contained in t.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

See also Metric.cthickening_eq_biUnion_closedBall.

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

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

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

For the equality, see infEdist_cthickening.

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

For the equality, see infEdist_thickening.

@[simp]

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

For the equality, see thickening_thickening.

@[simp]

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

For the equality, see thickening_cthickening.

@[simp]

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

For the equality, see cthickening_thickening.

@[simp]

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

For the equality, see cthickening_cthickening.

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