Theorems · Theorem · general topology

exists_locallyFinite_subset_iUnion_ball_radius_lt

∀ {α : Type u} [inst : MetricSpace α] [ProperSpace α] {s : Set α},
  IsClosed s →
    ∀ {R : α → ℝ},
      (∀ x ∈ s, 0 < R x) →
        ∃ ι c r r',
          (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
            (LocallyFinite fun i => Metric.ball (c i) (r' i)) ∧ s ⊆ ⋃ i, Metric.ball (c i) (r i)

Let R : α → ℝ be a (possibly discontinuous) function on a proper metric space. Let s be a closed set in α such that R is positive on s. Then there exists a collection of pairs of balls Metric.ball (c i) (r i), Metric.ball (c i) (r' i) such that * all centers belong to s; * for all i we have 0 < r i < r' i < R (c i); * the family of balls Metric.ball (c i) (r' i) is locally finite; * the balls Metric.ball (c i) (r i) cover s. This is a simple corollary of refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set and exists_subset_iUnion_ball_radius_pos_lt.

Defined in

Mathlib.Topology.MetricSpace.ShrinkingLemma

Cited by

1 results in Mathlib

Foundations

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

Assumes

MetricSpaceProperSpace