English
Let la, lb be filters and f: α → Filter β. The statement Tendsto f la (𝓝 lb) holds iff for every s ∈ lb, the set {a ∈ α : s ∈ f a} is eventually true along la; i.e., ∀ s ∈ lb, ∀ᶠ a in la, s ∈ f a.
Русский
Пусть la, lb — фильтры и f: α → Filter β. Тождество Tendsto f la (𝓝 lb) эквивалентно тому, что для каждого s ∈ lb множество {a : s ∈ f a} встречается «наконец» вдоль la: ∀ s ∈ lb, ∀ᶠ a in la, s ∈ f a.
LaTeX
$$$\mathrm{Tendsto}\ f\ la\ (\mathcal{N}\ lb) \iff \forall s\in lb,\forall^{\mathbf{f}} a\in la,\ s\in f(a).$$$
Lean4
protected theorem tendsto_nhds {la : Filter α} {lb : Filter β} {f : α → Filter β} :
Tendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ a in la, s ∈ f a := by simp only [nhds_eq', tendsto_lift', mem_setOf_eq]
