eventually_nhds_iff — Mathlib

English

A property holds eventually in the neighborhood filter of x if and only if there exists ε>0 such that the property holds for all points within the ball around x of radius ε.

Русский

Свойство выполняется единично в окрестности x тогда и только тогда, когда существует ε>0, такое что свойство выполняется для всех точек внутри шара вокруг x радиуса ε.

LaTeX

$$$$ \text{Eventually}(p, \mathcal{N}(x)) \iff \exists \varepsilon > 0, \forall y \in \mathrm{ball}(x, \varepsilon), p(y). $$$$

Lean4

theorem eventually_nhds_iff {p : α → Prop} : (∀ᶠ y in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ ⦃y⦄, dist y x < ε → p y :=
  mem_nhds_iff

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