English
If a property p holds for all points in closed balls of arbitrarily large radii around x, then p holds for every y in the space.
Русский
Если свойство p выполняется для всех точек в замкнутых шарах вокруг x радиусом, стремящимся к бесконечности, тогда p выполняется для любой точки пространства.
LaTeX
$$$ (p: \alpha \to \text{Prop}) \,\to\, (x: \alpha) \,\to\, (H: \exists^\infty R \text{ in } atTop, \forall y \in \overline{B}(x,R), p(y)) \,\to\, \forall y, p(y) $$$
Lean4
/-- If a property holds for all points in closed balls of arbitrarily large radii, then it holds for
all points. -/
theorem forall_of_forall_mem_closedBall (p : α → Prop) (x : α) (H : ∃ᶠ R : ℝ in atTop, ∀ y ∈ closedBall x R, p y)
(y : α) : p y :=
by
obtain ⟨R, hR, h⟩ : ∃ R ≥ dist y x, ∀ z : α, z ∈ closedBall x R → p z := frequently_iff.1 H (Ici_mem_atTop (dist y x))
exact h _ hR
