Theorems · Theorem · general topology

Metric.eventually_nhds_zero_forall_closedEBall_subset

∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K →
          ∀ (x : X), ∀ᶠ (p : ENNReal × X) in nhds 0 ×ˢ nhds x, ∀ (i : ι), p.2 ∈ K i → Metric.closedEBall 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 Metric.closedEBall y r ⊆ U i.

Defined in

Mathlib.Topology.MetricSpace.PartitionOfUnity

Cited by

2 results in Mathlib

Foundations

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

Assumes

EMetricSpace