Thickenings

Compact pairwise disjoint sets in a finite family in an extended metric space admit pairwise disjoint thickenings of one common positive radius. This supplies uniformly separated neighborhoods, all of the same metric size. A locally finite family of pairwise disjoint compact sets still admits pairwise disjoint closed thickenings, with radii depending on the member (LocallyFinite.exists_cthickenings_pairwiseDisjoint). In a proper space, closed thickenings of the members of a locally finite family by bounded radii again form a locally finite family (LocallyFinite.cthickening).

In a pseudometric space, the closed δ-thickening of a nonempty set, for δ ≥ 0, consists of the points at distance at most δ from it (TauCeti.mem_cthickening_iff_infDist_le). This is the closed counterpart of Mathlib's Metric.mem_thickening_iff_infDist_lt, and describes closed thickenings as sublevel sets of the distance function, and their complements as strict superlevel sets (TauCeti.compl_cthickening_eq_setOf_lt_infDist).

A closed set in a pseudometric space is the intersection of an antitone sequence of open sets inside any set whose interior contains it, namely the intersections of that interior with thickenings of radii 1 / (n + 1) (IsClosed.exists_antitone_isOpen_iInter_eq).

On the real line, the terms of an injective two-sided sequence tending to -∞ and +∞ at its two ends have pairwise disjoint closed intervals around them forming a locally finite family (TauCeti.exists_closedBall_pairwiseDisjoint_locallyFinite). An open subset of X × ℝ containing a vertical line contains a tube around it, whose radius is locally bounded below by positive constants (IsOpen.exists_tube_subset).

For an open set s with nonempty complement and δ → 0, the sets {y | δ < infDist y sᶜ} exhaust s from the inside, eventually containing a ball around each point of s (IsOpen.exists_eventually_closedBall_subset_setOf_lt_infDist). If s is moreover bounded in a proper space, a function continuous on closure s and at most m on frontier s is below m + η near the complement of s (IsOpen.exists_pos_forall_lt_add_of_infDist_lt). Under a K-Lipschitz map, the R / K-thickening of a preimage lies in the preimage of the R-thickening (LipschitzWith.thickening_preimage_subset_preimage_thickening), and likewise for closed thickenings (LipschitzWith.cthickening_preimage_subset_preimage_cthickening).

theorem TauCeti.exists_thickenings_pairwiseDisjoint {X : Type u_1} {ι : Type u_2} [EMetricSpace X] [Finite ι] (K : ι → Set X) (hK : ∀ (i : ι), IsCompact (K i)) (hdisj : Pairwise (Function.onFun Disjoint K)) : ∃ (δ : ℝ), 0 < δ ∧ Pairwise (Function.onFun Disjoint fun (i : ι) => Metric.thickening δ (K i))

A finite family of pairwise disjoint compact sets in an extended metric space admits pairwise disjoint thickenings of one common positive radius. This extends Mathlib's two-set result Disjoint.exists_thickenings.

theorem TauCeti.mem_cthickening_iff_infDist_le {X : Type u_1} [PseudoMetricSpace X] {s : Set X} (hs : s.Nonempty) {δ : ℝ} (hδ : 0 ≤ δ) {x : X} : x ∈ Metric.cthickening δ s ↔ Metric.infDist x s ≤ δ

For δ ≥ 0, a point lies in the closed δ-thickening of a nonempty set exactly when its distance to the set is at most δ.

theorem TauCeti.compl_cthickening_eq_setOf_lt_infDist {X : Type u_1} [PseudoMetricSpace X] {s : Set X} (hs : s.Nonempty) {δ : ℝ} (hδ : 0 ≤ δ) : (Metric.cthickening δ s)ᶜ = {x : X | δ < Metric.infDist x s}

For δ ≥ 0, the complement of the closed δ-thickening of a nonempty set consists of the points at distance more than δ from it.

theorem LipschitzWith.thickening_preimage_subset_preimage_thickening {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {K : NNReal} {R : ℝ} (hf : LipschitzWith K f) (S : Set Y) : Metric.thickening (R / ↑K) (f ⁻¹' S) ⊆ f ⁻¹' Metric.thickening R S

Under a K-Lipschitz map, the R / K-thickening of a preimage lies in the preimage of the R-thickening.

theorem LipschitzWith.cthickening_preimage_subset_preimage_cthickening {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {K : NNReal} {R : ℝ} (hf : LipschitzWith K f) (S : Set Y) : Metric.cthickening (R / ↑K) (f ⁻¹' S) ⊆ f ⁻¹' Metric.cthickening R S

Under a K-Lipschitz map, the closed R / K-thickening of a preimage lies in the preimage of the closed R-thickening.

theorem IsClosed.exists_antitone_isOpen_iInter_eq {X : Type u_1} [PseudoMetricSpace X] {K L : Set X} (hK : IsClosed K) (hKL : K ⊆ interior L) : ∃ (W : ℕ → Set X), (∀ (n : ℕ), IsOpen (W n)) ∧ (∀ (n : ℕ), W n ⊆ L) ∧ (∀ (n : ℕ), K ⊆ W n) ∧ Antitone W ∧ ⋂ (n : ℕ), W n = K

A closed set K in a pseudometric space contained in the interior of a set L is the intersection of an antitone sequence of open sets W n with K ⊆ W n ⊆ L.

theorem LocallyFinite.exists_cthickenings_pairwiseDisjoint {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K : ι → Set X} (hK : ∀ (i : ι), IsCompact (K i)) (hdisj : Pairwise (Function.onFun Disjoint K)) (hlf : LocallyFinite K) : ∃ (δ : ι → ℝ), (∀ (i : ι), 0 < δ i) ∧ Pairwise (Function.onFun Disjoint fun (i : ι) => Metric.cthickening (δ i) (K i))

A locally finite family of pairwise disjoint compact sets in an extended metric space admits pairwise disjoint closed thickenings, of positive radii depending on the member. This extends Mathlib's two-set result Disjoint.exists_cthickenings.

theorem LocallyFinite.cthickening {ι : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [ProperSpace X] {f : ι → Set X} (hf : LocallyFinite f) {δ : ι → ℝ} {R : ℝ} (hδ : ∀ (i : ι), δ i ≤ R) : LocallyFinite fun (i : ι) => Metric.cthickening (δ i) (f i)

In a proper space, the closed thickenings of the members of a locally finite family by radii bounded above form a locally finite family.

theorem TauCeti.exists_closedBall_pairwiseDisjoint_locallyFinite (x : ℤ → ℝ) (hx : Function.Injective x) (htop : Filter.Tendsto x Filter.atTop Filter.atTop) (hbot : Filter.Tendsto x Filter.atBot Filter.atBot) : ∃ (ε : ℤ → ℝ), (∀ (ν : ℤ), 0 < ε ν ∧ ε ν ≤ 1) ∧ Pairwise (Function.onFun Disjoint fun (ν : ℤ) => Metric.closedBall (x ν) (ε ν)) ∧ LocallyFinite fun (ν : ℤ) => Metric.closedBall (x ν) (ε ν)

Around the terms of an injective two-sided sequence of reals tending to -∞ and to +∞ at its two ends, there are closed intervals of positive radii at most 1 which are pairwise disjoint and form a locally finite family.

theorem IsOpen.exists_tube_subset {X : Type u_1} [PseudoMetricSpace X] {c : X} {W : Set (X × ℝ)} (hW : IsOpen W) (hcW : ∀ (t : ℝ), (c, t) ∈ W) : ∃ (γ : ℝ → ℝ), (∀ (x : ℝ), ∃ r > 0, ∀ᶠ (y : ℝ) in nhds x, r ≤ γ y) ∧ ∀ (u : X) (t : ℝ), dist u c ≤ γ t → (u, t) ∈ W

Tubes around a vertical line. An open subset W of X × ℝ containing the vertical line through c contains a tube {(u, t) | dist u c ≤ γ t} around that line, whose radius γ is locally bounded below by positive constants.

theorem IsOpen.exists_eventually_closedBall_subset_setOf_lt_infDist {X : Type u_1} {ι : Type u_2} [PseudoMetricSpace X] {s : Set X} (hs : IsOpen s) (hc : sᶜ.Nonempty) {l : Filter ι} {δ : ι → ℝ} (hδ : Filter.Tendsto δ l (nhds 0)) {z : X} (hz : z ∈ s) : ∃ r > 0, ∀ᶠ (i : ι) in l, Metric.closedBall z r ⊆ {y : X | δ i < Metric.infDist y sᶜ}

Interior exhaustion by the distance to the complement. If δ tends to 0, then every point z of an open set s with nonempty complement has a closed ball around it which eventually lies in {y | δ i < infDist y sᶜ}.

theorem IsOpen.exists_pos_forall_lt_add_of_infDist_lt {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : IsOpen s) (hb : Bornology.IsBounded s) (hc : sᶜ.Nonempty) {f : X → ℝ} (hf : ContinuousOn f (closure s)) {m : ℝ} (hm : ∀ z ∈ frontier s, f z ≤ m) {η : ℝ} (hη : 0 < η) : ∃ δ > 0, ∀ z ∈ s, Metric.infDist z sᶜ < δ → f z < m + η

Values near the frontier. Let f be continuous on the closure of a bounded open set s with nonempty complement in a proper space, and at most m on the frontier of s. Then for every η > 0, f < m + η at the points of s close enough to the complement of s.