English
In a proper metric space, a point-finite open cover by balls can be refined to a cover by smaller balls using the same index set.
Русский
В корректном метрическом пространстве точечное конечное покрытие шарообразными окрестностями можно сузить до покрытия меньшими шарами с тем же индексным множеством.
LaTeX
$$$\\exists r' : ι \\to \\mathbb{R},\\ ⋃ i, \\mathrm{ball}(c_i,r'_i) = \\mathbb{U}niv \\\\land \\forall i, r'_i < r_i$$$
Lean4
/-- 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. -/
theorem exists_iUnion_ball_eq_radius_lt {r : ι → ℝ} (uf : ∀ x, {i | x ∈ ball (c i) (r i)}.Finite)
(uU : ⋃ i, ball (c i) (r i) = univ) : ∃ r' : ι → ℝ, ⋃ i, ball (c i) (r' i) = univ ∧ ∀ i, r' i < r i :=
let ⟨r', hU, hv⟩ := exists_subset_iUnion_ball_radius_lt isClosed_univ (fun x _ => uf x) uU.ge
⟨r', univ_subset_iff.1 hU, hv⟩
