Theorems · Theorem · general topology

Metric.exists_continuous_nnreal_forall_closedBall_subset

∀ {ι : Type u_1} {X : Type u_2} [inst : MetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K → ∃ δ, (∀ (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.

Defined in

Mathlib.Topology.MetricSpace.PartitionOfUnity

Cited by

1 results in Mathlib

Foundations

Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MetricSpace