Theorems · Theorem · general topology

exists_subset_iUnion_ball_radius_lt

∀ {α : Type u} {ι : Type v} [inst : MetricSpace α] [ProperSpace α] {c : ι → α} {s : Set α} {r : ι → ℝ},
  IsClosed s →
    (∀ x ∈ s, {i | x ∈ Metric.ball (c i) (r i)}.Finite) →
      s ⊆ ⋃ i, Metric.ball (c i) (r i) → ∃ r', s ⊆ ⋃ i, Metric.ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a closed subset of a proper metric space by open balls can be shrunk to a new cover by open balls so that each of the new balls has strictly smaller radius than the old one. This version assumes that fun x ↦ ball (c i) (r i) is a locally finite covering and provides a covering indexed by the same type.

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