tendsto_nhds_nhds — Mathlib

English

In a normed group, Tendsto f (nhds x) (nhds y) is equivalent to an epsilon-delta condition via norms

Русский

В нормированной группе схождение Tendsto эквивалентно условию по ε и δ через нормы

LaTeX

$$$\\operatorname{Tendsto} f (\\mathcal{nhds} x) (\\mathcal{nhds} y) \\iff \\forall \\varepsilon>0,\\: \\exists \\delta>0,\\: \\forall x',\\: \\|x'/x\\| < \\delta \\Rightarrow \\|f x'/y\\| < \\varepsilon$$$

Lean4

@[to_additive]
theorem tendsto_nhds_nhds {f : E → F} {x : E} {y : F} :
    Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x', ‖x' / x‖ < δ → ‖f x' / y‖ < ε := by
  simp_rw [Metric.tendsto_nhds_nhds, dist_eq_norm_div]

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