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 ∈ thickening δ s ↔ EMetric.infEdist x s < ENNReal.ofReal δ

theorem Metric.eventually_notMem_thickening_of_infEdist_pos {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : x ∉ closure E) : ∀ᶠ (δ : ℝ) in nhds 0, x ∉ 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 δ.

@[deprecated Metric.eventually_notMem_thickening_of_infEdist_pos (since := "2025-05-23")]

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

Alias of Metric.eventually_notMem_thickening_of_infEdist_pos.

---

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

The (open) thickening is an open set.

@[simp]

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

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

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

theorem Metric.thickening_mono {α : Type u} [PseudoEMetricSpace α] {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : Set α) : thickening δ₁ E ⊆ 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₁ E₂ : Set α} (h : E₁ ⊆ E₂) : thickening δ E₁ ⊆ 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 ∈ thickening δ E ↔ ∃ z ∈ E, edist x z < ENNReal.ofReal δ

theorem Metric.frontier_thickening_subset {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : ℝ} : frontier (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 (Function.onFun Disjoint fun (r : ℝ) => frontier (thickening r A))

theorem Metric.subset_compl_thickening_compl_thickening_self {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : E ⊆ (thickening δ (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 α) : thickening δ (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 ∈ thickening δ E ↔ infDist x E < δ

theorem Metric.mem_thickening_iff {δ : ℝ} {X : Type u} [PseudoMetricSpace X] {E : Set X} {x : X} : x ∈ 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) : thickening δ {x} = ball x δ

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

theorem Metric.thickening_eq_biUnion_ball {X : Type u} [PseudoMetricSpace X] {δ : ℝ} {E : Set X} : thickening δ E = ⋃ x ∈ E, 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 : IsBounded E) : 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 ∈ cthickening δ s ↔ EMetric.infEdist x s ≤ ENNReal.ofReal δ

theorem Metric.eventually_notMem_cthickening_of_infEdist_pos {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : x ∉ closure E) : ∀ᶠ (δ : ℝ) in nhds 0, x ∉ 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 δ.

@[deprecated Metric.eventually_notMem_cthickening_of_infEdist_pos (since := "2025-05-23")]

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

Alias of Metric.eventually_notMem_cthickening_of_infEdist_pos.

---

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 ∈ 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 ∈ cthickening δ E

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

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

The closed thickening is a closed set.

@[simp]

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

The closed thickening of the empty set is empty.

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

@[simp]

theorem Metric.cthickening_zero {α : Type u} [PseudoEMetricSpace α] (E : Set α) : 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 α) : cthickening (max 0 δ) E = cthickening δ E

theorem Metric.cthickening_mono {α : Type u} [PseudoEMetricSpace α] {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : Set α) : cthickening δ₁ E ⊆ 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 ≤ δ) : cthickening δ {x} = closedBall x δ

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

theorem Metric.cthickening_subset_of_subset {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) {E₁ E₂ : Set α} (h : E₁ ⊆ E₂) : cthickening δ E₁ ⊆ 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 α) : cthickening (↑δ₁) E ⊆ thickening δ₂ E

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

theorem Bornology.IsBounded.cthickening {α : Type u_2} [PseudoMetricSpace α] {δ : ℝ} {E : Set α} (h : IsBounded E) : 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 α) : thickening δ E ⊆ interior (cthickening δ E)

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

theorem Metric.closure_subset_cthickening {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : closure E ⊆ 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 ⊆ 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 ⊆ thickening δ E

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

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

A set is contained in its own closed thickening.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

theorem Metric.thickening_eq_empty_iff_of_pos {α : Type u} [PseudoEMetricSpace α] {ε : ℝ} {s : Set α} (hε : 0 < ε) : thickening ε s = ∅ ↔ s = ∅

theorem Metric.thickening_nonempty_iff_of_pos {α : Type u} [PseudoEMetricSpace α] {ε : ℝ} {s : Set α} (hε : 0 < ε) : (thickening ε s).Nonempty ↔ s.Nonempty

@[simp]

theorem Metric.thickening_eq_empty_iff {α : Type u} [PseudoEMetricSpace α] {ε : ℝ} {s : Set α} : thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅

@[simp]

theorem Metric.thickening_nonempty_iff {α : Type u} [PseudoEMetricSpace α] {ε : ℝ} {s : Set α} : (thickening ε s).Nonempty ↔ 0 < ε ∧ s.Nonempty

theorem Disjoint.exists_thickenings {α : Type u} [PseudoEMetricSpace α] {s 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 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 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 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 (δ : ℝ) => thickening δ K

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

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

theorem Metric.cthickening_eq_iInter_cthickening {α : Type u} [PseudoEMetricSpace α] {δ : ℝ} (E : Set α) : cthickening δ E = ⋂ (ε : ℝ), ⋂ (_ : δ < ε), 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 α) : cthickening δ E = ⋂ ε ∈ s, thickening ε E

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

theorem Metric.cthickening_eq_iInter_thickening'' {α : Type u} [PseudoEMetricSpace α] (δ : ℝ) (E : Set α) : cthickening δ E = ⋂ (ε : ℝ), ⋂ (_ : max 0 δ < ε), 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, 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 < δ), 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, 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 < δ), 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 (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) (δ : ℝ) : closedBall x δ ⊆ 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δδ' : δ < δ') : cthickening δ E ⊆ ⋃ x ∈ E, 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 ≤ δ) : cthickening δ E = ⋃ x ∈ closure E, 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 (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 (thickening δ s) + ENNReal.ofReal δ

For the equality, see infEdist_thickening.

@[simp]

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

For the equality, see thickening_thickening.

@[simp]

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

For the equality, see thickening_cthickening.

@[simp]

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

For the equality, see cthickening_thickening.

@[simp]

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

For the equality, see cthickening_cthickening.

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

theorem Metric.thickening_ball {α : Type u} [PseudoMetricSpace α] (x : α) (ε δ : ℝ) : thickening ε (ball x δ) ⊆ ball x (ε + δ)

theorem IsClopen.of_thickening_subset_self {α : Type u} [PseudoEMetricSpace α] {s : Set α} {δ : ℝ} (hδ : 0 < δ) (hs : Metric.thickening δ s ⊆ s) : IsClopen s

theorem IsClopen.of_cthickening_subset_self {α : Type u} [PseudoEMetricSpace α] {s : Set α} {δ : ℝ} (hδ : 0 < δ) (hs : Metric.cthickening δ s ⊆ s) : IsClopen s

theorem IsCompact.exists_thickening_image_subset {α : Type u} [PseudoEMetricSpace α] {β : Type u_2} [PseudoEMetricSpace β] {f : α → β} {K : Set α} {U : Set β} (hK : IsCompact K) (ho : IsOpen U) (hf : ∀ x ∈ K, ContinuousAt f x) (hKU : Set.MapsTo f K U) : ∃ ε > 0, ∃ V ∈ nhdsSet K, Metric.thickening ε (f '' V) ⊆ U