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

source

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.

source

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}

source

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})

source

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.

source

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.

source

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.

source

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.

source

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.