English
If u is a neighborhood of x in a metric space, then for sufficiently small r, the closed ball around x with radius r is contained in u.
Русский
Если u — окрестность точки x в метрическом пространстве, то для достаточно малого радиуса r замкнутый шар вокруг x лежит внутри u.
LaTeX
$$$\exists \varepsilon>0\,\, (\overline{B}(x,\varepsilon) \subseteq u)$$$
Lean4
/-- If `u` is a neighborhood of `x`, then for small enough `r`, the closed ball
`Metric.closedBall x r` is contained in `u`. -/
theorem eventually_closedBall_subset {x : α} {u : Set α} (hu : u ∈ 𝓝 x) : ∀ᶠ r in 𝓝 (0 : ℝ), closedBall x r ⊆ u :=
by
obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu
have : Iic ε ∈ 𝓝 (0 : ℝ) := Iic_mem_nhds εpos
filter_upwards [this] with _ hr using Subset.trans (closedBall_subset_closedBall hr) hε
