English
If each r_i > 0, a closed set s covered by balls can be refined to smaller balls with radii r'_i ∈ (0, r_i).
Русский
Если каждый радиус r_i положителен, то можно найти r'_i ∈ (0, r_i) такие, что покрытие по меньшим шарам продолжает покрывать s.
LaTeX
$$$\\exists r' : ι \\to \\mathbb{R},\\ (s \\subseteq \\bigcup_i \\mathrm{ball}(c_i,r'_i))\\land \\forall i, r'_i \\in Ioo(0, 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 nonempty open balls can be shrunk to a new cover by
nonempty open balls so that each of the new balls has strictly smaller radius than the old one. -/
theorem exists_subset_iUnion_ball_radius_pos_lt {r : ι → ℝ} (hr : ∀ i, 0 < r i) (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 ∈ Ioo 0 (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_pos_lt_subset_ball (hr i) (hvc i) (hcv i)
choose r' hlt hsub using this
exact ⟨r', hsv.trans <| iUnion_mono hsub, hlt⟩
