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} [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 → EMetric.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} [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 | EMetric.closedBall y r ⊆ U i}

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 | EMetric.closedBall y r ⊆ U i})

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, 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} [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, 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} [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, 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} [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, 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} [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, 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.