English
A function tends to a limit with respect to nhdsWithin if and only if a quantified condition on ε and δ holds for all x in s.
Русский
Функция стремится к пределу относительно nhdsWithin, если и только если выполняется заданное условие на ε и δ для всех x∈s.
LaTeX
$$$\\mathrm{Tendsto}\,f\\,(\\mathcal{N}[s]a)\\,(\\mathcal{N}[t]b) \\iff \\forall \\varepsilon>0, \\exists \\delta>0, \\forall \\{x\\}, x\\in s \\to \\operatorname{edist}(x,a) < \\delta \\to (f(x)\\in t \\land \\operatorname{edist}(f(x),b) < \\varepsilon)$$$
Lean4
theorem tendsto_nhdsWithin_nhdsWithin {t : Set β} {a b} :
Tendsto f (𝓝[s] a) (𝓝[t] b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x⦄, x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε :=
(nhdsWithin_basis_eball.tendsto_iff nhdsWithin_basis_eball).trans <|
forall₂_congr fun ε _ => exists_congr fun δ => and_congr_right fun _ => forall_congr' fun x => by simp; tauto
