forall_of_forall_mem_ball — Mathlib

English

If a property p holds for all points in balls of arbitrarily large radii around x, then p holds for every y.

Русский

Если свойство p выполняется для всех точек в шарax радиусом, стремящимся к бесконечности, то p выполняется для любой точки y.

LaTeX

$$$ (p: \alpha \to \text{Prop}) \,\to\, (x: \alpha) \,\to\, (H: \exists^\infty R \text{ in } atTop, \forall y \in B(x,R), p(y)) \,\to\, \forall y, p(y) $$$

Lean4

/-- If a property holds for all points in balls of arbitrarily large radii, then it holds for all
points. -/
theorem forall_of_forall_mem_ball (p : α → Prop) (x : α) (H : ∃ᶠ R : ℝ in atTop, ∀ y ∈ ball x R, p y) (y : α) : p y :=
  by
  obtain ⟨R, hR, h⟩ : ∃ R > dist y x, ∀ z : α, z ∈ ball x R → p z := frequently_iff.1 H (Ioi_mem_atTop (dist y x))
  exact h _ hR

Похожие утверждения