English
Characterizes convergence to a via neighborhood realizers: Tendsto m f (nhds a) iff for every t in R.F, a ∈ R.F t implies there exists s such that for all x in F.F s, m x ∈ R.F t.
Русский
Характеризует схождение к a через реализаторы окрестностей: Tendsto m f (nhds a) эквивалентно существованию для каждого t ∈ R.F такого s, что для всех x ∈ F.F s выполняется m x ∈ R.F t.
LaTeX
$$$\mathrm{Tendsto}\, m\, f\, (\mathcal{N}a) \iff \forall t, a \in R.F t \to \exists s, \forall x \in F.F s, m x \in R.F t.$$$
Lean4
theorem tendsto_nhds_iff {m : β → α} {f : Filter β} (F : f.Realizer) (R : Realizer α) {a : α} :
Tendsto m f (𝓝 a) ↔ ∀ t, a ∈ R.F t → ∃ s, ∀ x ∈ F.F s, m x ∈ R.F t :=
(F.tendsto_iff _ (R.nhds a)).trans Subtype.forall
