Lemmas about (e)metric spaces that need partition of unity

The main lemma in this file (see Metric.exists_continuous_real_forall_closedBall_subset) says the following. Let X be a metric space. Let K : ι → Set X be a locally finite family of closed sets, let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive continuous function δ : C(X, ℝ) such that for any i and x ∈ K i, we have Metric.closedBall x (δ x) ⊆ U i. We also formulate versions of this lemma for extended metric spaces and for different codomains (ℝ, ℝ≥0, and ℝ≥0∞).

We also prove a few auxiliary lemmas to be used later in a proof of the smooth version of this lemma.

Tags

metric space, partition of unity, locally finite

theorem Metric.eventually_nhds_zero_forall_closedEBall_subset {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) (x : X) : ∀ᶠ (p : ENNReal × X) in nhds 0 ×ˢ nhds x, ∀ (i : ι), p.2 ∈ K i → closedEBall p.2 p.1 ⊆ U i

Let K : ι → Set X be a locally finite family of closed sets in an emetric space. Let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then for any point x : X, for sufficiently small r : ℝ≥0∞ and for y sufficiently close to x, for all i, if y ∈ K i, then Metric.closedEBall y r ⊆ U i.

theorem Metric.exists_forall_closedEBall_subset_aux₁ {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) (x : X) : ∃ (r : ℝ), ∀ᶠ (y : X) in nhds x, r ∈ Set.Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ENNReal | closedEBall y r ⊆ U i}

Auxuliary lemma for exists_continuous_real_forall_closedEBall_subset and its smooth counterpart.

theorem Metric.exists_forall_closedEBall_subset_aux₂ {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (y : X) : Convex ℝ (Set.Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ENNReal | closedEBall y r ⊆ U i})

Auxuliary lemma for exists_continuous_real_forall_closedEBall_subset and its smooth counterpart.

theorem Metric.exists_continuous_real_forall_closedEBall_subset {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) : ∃ (δ : C(X, ℝ)), (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i

Let X be an extended metric space. Let K : ι → Set X be a locally finite family of closed sets, let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive continuous function δ : C(X, ℝ) such that for any i and x ∈ K i, we have Metric.closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i.

theorem Metric.exists_continuous_nnreal_forall_closedEBall_subset {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) : ∃ (δ : C(X, NNReal)), (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedEBall x ↑(δ x) ⊆ U i

Let X be an extended metric space. Let K : ι → Set X be a locally finite family of closed sets, let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive continuous function δ : C(X, ℝ≥0) such that for any i and x ∈ K i, we have Metric.closedEBall x (δ x) ⊆ U i.

theorem Metric.exists_continuous_ennreal_forall_closedEBall_subset {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) : ∃ (δ : C(X, ENNReal)), (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedEBall x (δ x) ⊆ U i

Let X be an extended metric space. Let K : ι → Set X be a locally finite family of closed sets, let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive continuous function δ : C(X, ℝ≥0∞) such that for any i and x ∈ K i, we have Metric.closedEBall x (δ x) ⊆ U i.

@[deprecated Metric.eventually_nhds_zero_forall_closedEBall_subset (since := "2026-01-24")]

theorem EMetric.eventually_nhds_zero_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) (x : X) : ∀ᶠ (p : ENNReal × X) in nhds 0 ×ˢ nhds x, ∀ (i : ι), p.2 ∈ K i → Metric.closedEBall p.2 p.1 ⊆ U i

Alias of Metric.eventually_nhds_zero_forall_closedEBall_subset.

---

Let K : ι → Set X be a locally finite family of closed sets in an emetric space. Let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then for any point x : X, for sufficiently small r : ℝ≥0∞ and for y sufficiently close to x, for all i, if y ∈ K i, then Metric.closedEBall y r ⊆ U i.

@[deprecated Metric.exists_forall_closedEBall_subset_aux₁ (since := "2026-01-24")]

theorem EMetric.exists_forall_closedBall_subset_aux₁ {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) (x : X) : ∃ (r : ℝ), ∀ᶠ (y : X) in nhds x, r ∈ Set.Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ENNReal | Metric.closedEBall y r ⊆ U i}

Alias of Metric.exists_forall_closedEBall_subset_aux₁.

---

Auxuliary lemma for exists_continuous_real_forall_closedEBall_subset and its smooth counterpart.

@[deprecated Metric.exists_forall_closedEBall_subset_aux₂ (since := "2026-01-24")]

theorem EMetric.exists_forall_closedBall_subset_aux₂ {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (y : X) : Convex ℝ (Set.Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ENNReal | Metric.closedEBall y r ⊆ U i})

Alias of Metric.exists_forall_closedEBall_subset_aux₂.

---

Auxuliary lemma for exists_continuous_real_forall_closedEBall_subset and its smooth counterpart.

@[deprecated Metric.exists_continuous_real_forall_closedEBall_subset (since := "2026-01-24")]

theorem EMetric.exists_continuous_real_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) : ∃ (δ : C(X, ℝ)), (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i

Alias of Metric.exists_continuous_real_forall_closedEBall_subset.

---

Let X be an extended metric space. Let K : ι → Set X be a locally finite family of closed sets, let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive continuous function δ : C(X, ℝ) such that for any i and x ∈ K i, we have Metric.closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i.

@[deprecated Metric.exists_continuous_nnreal_forall_closedEBall_subset (since := "2026-01-24")]

theorem EMetric.exists_continuous_nnreal_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) : ∃ (δ : C(X, NNReal)), (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x ↑(δ x) ⊆ U i

Alias of Metric.exists_continuous_nnreal_forall_closedEBall_subset.

---

Let X be an extended metric space. Let K : ι → Set X be a locally finite family of closed sets, let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive continuous function δ : C(X, ℝ≥0) such that for any i and x ∈ K i, we have Metric.closedEBall x (δ x) ⊆ U i.

@[deprecated Metric.exists_continuous_ennreal_forall_closedEBall_subset (since := "2026-01-24")]

theorem EMetric.exists_continuous_eNNReal_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) : ∃ (δ : C(X, ENNReal)), (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x (δ x) ⊆ U i

Alias of Metric.exists_continuous_ennreal_forall_closedEBall_subset.

---

Let X be an extended metric space. Let K : ι → Set X be a locally finite family of closed sets, let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive continuous function δ : C(X, ℝ≥0∞) such that for any i and x ∈ K i, we have Metric.closedEBall x (δ x) ⊆ U i.

theorem Metric.exists_continuous_nnreal_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [MetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) : ∃ (δ : C(X, NNReal)), (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x ↑(δ x) ⊆ U i

Let X be a metric space. Let K : ι → Set X be a locally finite family of closed sets, let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive continuous function δ : C(X, ℝ≥0) such that for any i and x ∈ K i, we have Metric.closedBall x (δ x) ⊆ U i.

theorem Metric.exists_continuous_real_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [MetricSpace X] {K U : ι → Set X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) : ∃ (δ : C(X, ℝ)), (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x (δ x) ⊆ U i

Let X be a metric space. Let K : ι → Set X be a locally finite family of closed sets, let U : ι → Set X be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive continuous function δ : C(X, ℝ) such that for any i and x ∈ K i, we have Metric.closedBall x (δ x) ⊆ U i.