English
Let K_i be closed and U_i open with K_i ⊆ U_i, and {K_i} locally finite. Then around any x, there exists a positive radius r such that for y near x with y ∈ K_i for any i, the closed ball centered at y with radius r is contained in U_i for all such i.
Русский
Пусть K_i — замкнутыe, U_i — открыты и K_i ⊆ U_i, familienna lokalna finiteness. Тогда около любой точки x существует положительный радиус r, такой что для близких к x точек y, удовлетворяющих y ∈ K_i, шар с центром y и радиусом r lies внутри U_i для всех таких i.
LaTeX
$$$\\exists r > 0, \\ \\forall y \\text{ near } x,\\ \\forall i,\\ y \\in K_i \\Rightarrow \\overline{B}(y,r) \\subseteq U_i$$$
Lean4
/-- Let `K : ι → Set X` be a locally finite family of closed sets in an emetric space. Let
`U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then for any point
`x : X`, for sufficiently small `r : ℝ≥0∞` and for `y` sufficiently close to `x`, for all `i`, if
`y ∈ K i`, then `EMetric.closedBall y r ⊆ U i`. -/
theorem eventually_nhds_zero_forall_closedBall_subset (hK : ∀ i, IsClosed (K i)) (hU : ∀ i, IsOpen (U i))
(hKU : ∀ i, K i ⊆ U i) (hfin : LocallyFinite K) (x : X) :
∀ᶠ p : ℝ≥0∞ × X in 𝓝 0 ×ˢ 𝓝 x, ∀ i, p.2 ∈ K i → closedBall p.2 p.1 ⊆ U i :=
by
suffices ∀ i, x ∈ K i → ∀ᶠ p : ℝ≥0∞ × X in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
by
apply
mp_mem ((eventually_all_finite (hfin.point_finite x)).2 this)
(mp_mem (@tendsto_snd ℝ≥0∞ _ (𝓝 0) _ _ (hfin.iInter_compl_mem_nhds hK x)) _)
apply univ_mem'
rintro ⟨r, y⟩ hxy hyU i hi
simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy
exact hyU _ (hxy _ hi)
intro i hi
rcases nhds_basis_closed_eball.mem_iff.1 ((hU i).mem_nhds <| hKU i hi) with ⟨R, hR₀, hR⟩
rcases ENNReal.lt_iff_exists_nnreal_btwn.mp hR₀ with ⟨r, hr₀, hrR⟩
filter_upwards [prod_mem_prod (eventually_lt_nhds hr₀) (closedBall_mem_nhds x (tsub_pos_iff_lt.2 hrR))] with p hp z hz
apply hR
calc
edist z x ≤ edist z p.2 + edist p.2 x := edist_triangle _ _ _
_ ≤ p.1 + (R - p.1) := (add_le_add hz <| le_trans hp.2 <| tsub_le_tsub_left hp.1.out.le _)
_ = R := add_tsub_cancel_of_le (lt_trans (by exact hp.1) hrR).le
