tendsto_nhds_nhds — Mathlib

English

Tendsto f from nhds a to nhds b is characterized by an ε–δ condition using edist and ε > 0.

Русский

Стремление f из nhds a в nhds b характеризуется условием ε–δ с использованием edist и ε > 0.

LaTeX

$$$\\mathrm{Tendsto}\,f\\,(\\mathcal{N}a)\\,(\\mathcal{N}b) \\iff \\forall \\varepsilon>0, \\exists \\delta>0, \\forall x, \\operatorname{edist}(x,a) < \\delta \\Rightarrow \\operatorname{edist}(f(x),b) < \\varepsilon$$$

Lean4

theorem tendsto_nhds_nhds {a b} : Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x⦄, edist x a < δ → edist (f x) b < ε :=
  nhds_basis_eball.tendsto_iff nhds_basis_eball

Похожие утверждения