# 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 EMetric.eventually_nhds_zero_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [] {K : ιSet X} {U : ιSet X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : ) (x : X) :
∀ᶠ (p : ) in nhds 0 ×ˢ nhds x, ∀ (i : ι), p.2 K iEMetric.closedBall 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 EMetric.closedBall y r ⊆ U i.

theorem EMetric.exists_forall_closedBall_subset_aux₁ {ι : Type u_1} {X : Type u_2} [] {K : ιSet X} {U : ιSet X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : ) (x : X) :
∃ (r : ), ∀ᶠ (y : X) in nhds x, r ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y K i), {r : ENNReal | U i}
theorem EMetric.exists_forall_closedBall_subset_aux₂ {ι : Type u_1} {X : Type u_2} [] {K : ιSet X} {U : ιSet X} (y : X) :
Convex ( ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y K i), {r : ENNReal | U i})
theorem EMetric.exists_continuous_real_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [] {K : ιSet X} {U : ιSet X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : ) :
∃ (δ : ), (∀ (x : X), 0 < δ x) ∀ (i : ι), xK i, EMetric.closedBall 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 EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i.

theorem EMetric.exists_continuous_nnreal_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [] {K : ιSet X} {U : ιSet X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : ) :
∃ (δ : ), (∀ (x : X), 0 < δ x) ∀ (i : ι), xK i, EMetric.closedBall 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 EMetric.closedBall x (δ x) ⊆ U i.

theorem EMetric.exists_continuous_eNNReal_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [] {K : ιSet X} {U : ιSet X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : ) :
∃ (δ : ), (∀ (x : X), 0 < δ x) ∀ (i : ι), xK i, EMetric.closedBall 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 EMetric.closedBall x (δ x) ⊆ U i.

theorem Metric.exists_continuous_nnreal_forall_closedBall_subset {ι : Type u_1} {X : Type u_2} [] {K : ιSet X} {U : ιSet X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : ) :
∃ (δ : ), (∀ (x : X), 0 < δ x) ∀ (i : ι), xK i, Metric.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} [] {K : ιSet X} {U : ιSet X} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : ) :
∃ (δ : ), (∀ (x : X), 0 < δ x) ∀ (i : ι), xK i, Metric.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.