English
A version of Filter.eventually_prod_iff where the first filter consists of neighborhoods in a pseudometric space; it describes eventual behavior of a product with a second factor filtered by a product of neighborhoods.
Русский
Версия эквивалентности \(\text{eventually}_\text{prod}\) для первого фильтра, состоящего из окрестностей в псевдометрическом пространстве, описывающая поведение произведения при фильтрации второй компоненты.
LaTeX
$$$$ \text{Eventually}(p, \mathcal{N}(x) \times\! f) \iff \exists \varepsilon>0, \exists pa: \mathbb{N} \to \text{Prop}, (\forall i\in f, pa(i)) \land \forall \{x\}, dist(x,x) < \varepsilon \to \forall i, pa(i) \to p(i,x). $$$$
Lean4
theorem eventually_nhds_iff_ball {p : α → Prop} : (∀ᶠ y in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ y ∈ ball x ε, p y :=
mem_nhds_iff
