# mathlibdocumentation

topology.metric_space.partition_of_unity

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

The main lemma in this file (see metric.exists_continuous_real_forall_closed_ball_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.closed_ball 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_closed_ball_subset {ι : Type u_1} {X : Type u_2} {K U : ι → set X} (hK : ∀ (i : ι), is_closed (K i)) (hU : ∀ (i : ι), is_open (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : locally_finite K) (x : X) :
∀ᶠ (p : ennreal × X) in (nhds 0).prod (nhds x), ∀ (i : ι), p.snd K i U i

Let K : ι → set X be a locally finitie 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.closed_ball y r ⊆ U i.

theorem emetric.exists_forall_closed_ball_subset_aux₁ {ι : Type u_1} {X : Type u_2} {K U : ι → set X} (hK : ∀ (i : ι), is_closed (K i)) (hU : ∀ (i : ι), is_open (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : locally_finite K) (x : X) :
∃ (r : ), ∀ᶠ (y : X) in nhds x, r ennreal.of_real ⁻¹' ⋂ (i : ι) (hi : y K i), {r : ennreal | U i}
theorem emetric.exists_forall_closed_ball_subset_aux₂ {ι : Type u_1} {X : Type u_2} {K U : ι → set X} (y : X) :
(set.Ioi 0 ennreal.of_real ⁻¹' ⋂ (i : ι) (hi : y K i), {r : ennreal | U i})
theorem emetric.exists_continuous_real_forall_closed_ball_subset {ι : Type u_1} {X : Type u_2} {K U : ι → set X} (hK : ∀ (i : ι), is_closed (K i)) (hU : ∀ (i : ι), is_open (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : locally_finite K) :
∃ (δ : C(X, )), (∀ (x : X), 0 < δ x) ∀ (i : ι) (x : X), x K i (ennreal.of_real (δ 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.closed_ball x (ennreal.of_real (δ x)) ⊆ U i.

theorem emetric.exists_continuous_nnreal_forall_closed_ball_subset {ι : Type u_1} {X : Type u_2} {K U : ι → set X} (hK : ∀ (i : ι), is_closed (K i)) (hU : ∀ (i : ι), is_open (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : locally_finite K) :
∃ (δ : , (∀ (x : X), 0 < δ x) ∀ (i : ι) (x : X), x K i (δ 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.closed_ball x (δ x) ⊆ U i.

theorem emetric.exists_continuous_ennreal_forall_closed_ball_subset {ι : Type u_1} {X : Type u_2} {K U : ι → set X} (hK : ∀ (i : ι), is_closed (K i)) (hU : ∀ (i : ι), is_open (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : locally_finite K) :
∃ (δ : , (∀ (x : X), 0 < δ x) ∀ (i : ι) (x : X), x K i (δ 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.closed_ball x (δ x) ⊆ U i.

theorem metric.exists_continuous_nnreal_forall_closed_ball_subset {ι : Type u_1} {X : Type u_2} [metric_space X] {K U : ι → set X} (hK : ∀ (i : ι), is_closed (K i)) (hU : ∀ (i : ι), is_open (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : locally_finite K) :
∃ (δ : , (∀ (x : X), 0 < δ x) ∀ (i : ι) (x : X), x K i (δ 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.closed_ball x (δ x) ⊆ U i.

theorem metric.exists_continuous_real_forall_closed_ball_subset {ι : Type u_1} {X : Type u_2} [metric_space X] {K U : ι → set X} (hK : ∀ (i : ι), is_closed (K i)) (hU : ∀ (i : ι), is_open (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : locally_finite K) :
∃ (δ : C(X, )), (∀ (x : X), 0 < δ x) ∀ (i : ι) (x : X), x K i (δ 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.closed_ball x (δ x) ⊆ U i.