English
For any fixed y, the set of radii r>0 such that the closed ball centered at y of radius r is contained in each U_i (for which y ∈ K_i) is a convex subset of the real numbers.
Русский
Для фиксированной точки y множество радиусов r>0, для которых шар с центром в y и радиусом r целиком содержится в каждом U_i с условием y ∈ K_i, является выпуклым подмножеством действительных чисел.
LaTeX
$$$\\text{Convex}_{\\\\mathbb{R}} \\\\big( Ioi(0) \\\\cap \\\\bigcap_{i: y \\in K_i} \\{ r \\\\mid \\\\overline{Ball}(y,r) \\subseteq U_i \\} \\big)$$$
Lean4
theorem exists_forall_closedBall_subset_aux₁ (hK : ∀ i, IsClosed (K i)) (hU : ∀ i, IsOpen (U i)) (hKU : ∀ i, K i ⊆ U i)
(hfin : LocallyFinite K) (x : X) :
∃ r : ℝ, ∀ᶠ y in 𝓝 x, r ∈ Ioi (0 : ℝ) ∩ ENNReal.ofReal ⁻¹' ⋂ (i) (_ : y ∈ K i), {r | closedBall y r ⊆ U i} :=
by
have :=
(ENNReal.continuous_ofReal.tendsto' 0 0 ENNReal.ofReal_zero).eventually
(eventually_nhds_zero_forall_closedBall_subset hK hU hKU hfin x).curry
rcases this.exists_gt with ⟨r, hr0, hr⟩
refine ⟨r, hr.mono fun y hy => ⟨hr0, ?_⟩⟩
rwa [mem_preimage, mem_iInter₂]
