English
In a normed group setting, a function f tends to y as x tends to x if and only if, for every ε > 0, there exists δ > 0 such that whenever ‖x' / x‖ < δ we have ‖f x' / y‖ < ε.
Русский
В нормированной группе функция f стремится к y при x→x тогда, когда для любого ε>0 существует δ>0, такое что при любых x' с ‖x'/x‖ < δ выполняется ‖f x' / y‖ < ε.
LaTeX
$$$\\operatorname{Tendsto} f (\\mathcal{nhds}\,x) (\\mathcal{nhds}\,y) \\\\ \\Longleftrightarrow \\forall \\varepsilon>0,\\: \\exists \\delta>0,\\: \\forall x',\\: \\|x'/x\\| < \\delta \\Rightarrow \\|f x' / y\\| < \\varepsilon$$$
Lean4
@[to_additive]
theorem tendsto_nhds_one {f : α → E} {l : Filter α} : Tendsto f l (𝓝 1) ↔ ∀ ε > 0, ∀ᶠ x in l, ‖f x‖ < ε :=
Metric.tendsto_nhds.trans <| by simp only [dist_one_right]
