English
A point-finite open cover of a closed subset by open balls in a proper metric space can be refined to a cover by smaller balls, still covering the set.
Русский
Пусть есть открытое покрытие замкнутого множества точками-окружностями баттона, конечная точечная пересечение; можно сузить радиусы так, чтобы новое покрытие имело меньшие радиусы и покрывало то же множество.
LaTeX
$$$\\exists r' : ι \\to \\mathbb{R},\\ (s \\subseteq \\bigcup_i \\mathrm{ball}(c_i,r'_i)) \\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 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. -/
theorem exists_subset_iUnion_ball_radius_lt {r : ι → ℝ} (hs : IsClosed s)
(uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite) (us : s ⊆ ⋃ i, ball (c i) (r i)) :
∃ r' : ι → ℝ, (s ⊆ ⋃ i, ball (c i) (r' i)) ∧ ∀ i, r' i < r i :=
by
rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with ⟨v, hsv, hvc, hcv⟩
have := fun i => exists_lt_subset_ball (hvc i) (hcv i)
choose r' hlt hsub using this
exact ⟨r', hsv.trans <| iUnion_mono <| hsub, hlt⟩
