mathlib3 documentation

topology.metric_space.partition_of_unity

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [emetric_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) :
∀ᶠ (p : ennreal × X) in (nhds 0).prod (nhds x), (i : ι), p.snd K i emetric.closed_ball p.snd p.fst 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} [emetric_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) :
(r : ), ∀ᶠ (y : X) in nhds x, r set.Ioi 0 ennreal.of_real ⁻¹' (i : ι) (hi : y K i), {r : ennreal | emetric.closed_ball y r U i}
theorem emetric.exists_forall_closed_ball_subset_aux₂ {ι : Type u_1} {X : Type u_2} [emetric_space X] {K U : ι set X} (y : X) :
convex (set.Ioi 0 ennreal.of_real ⁻¹' (i : ι) (hi : y K i), {r : ennreal | emetric.closed_ball y r U i})
theorem emetric.exists_continuous_real_forall_closed_ball_subset {ι : Type u_1} {X : Type u_2} [emetric_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 emetric.closed_ball x (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} [emetric_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, nnreal)), ( (x : X), 0 < δ x) (i : ι) (x : X), x K i emetric.closed_ball 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.closed_ball x (δ x) ⊆ U i.

theorem emetric.exists_continuous_ennreal_forall_closed_ball_subset {ι : Type u_1} {X : Type u_2} [emetric_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, ennreal)), ( (x : X), 0 < δ x) (i : ι) (x : X), x K i emetric.closed_ball 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.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) :
(δ : C(X, nnreal)), ( (x : X), 0 < δ x) (i : ι) (x : X), x K i metric.closed_ball 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.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 metric.closed_ball 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.closed_ball x (δ x) ⊆ U i.