Theorems · Theorem · general topology

exists_iUnion_ball_eq_radius_lt

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

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover 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.

Defined in

Mathlib.Topology.MetricSpace.ShrinkingLemma

Cited by

0 results in Mathlib

Foundations

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

Assumes

MetricSpaceProperSpace