tendsto_nhds — Mathlib

English

In a linearly ordered commutative group with the order topology, Tendsto f toward 𝓝(a) is equivalent to: for every ε > 1, eventually |f(b)/a|_m < ε along the filter x.

Русский

В линейно упорядоченной коммутативной группе с порядковой топологией переход f к 𝓝(a) эквивалентен тому, что для каждого ε>1 последовательность/поток имеет за пределами фильтра x значения |f(b)/a|_м < ε.

LaTeX

$$$$\forall {\alpha'},{\beta'}:\n \operatorname{Tendsto} f x (\mathcal{N} a) \\iff \\ \forall \varepsilon>1,\ \{b : |f(b)/a|_{m} < \varepsilon\} \in x.$$$$

Lean4

@[to_additive]
theorem tendsto_nhds {x : Filter β} {a : α} : Tendsto f x (𝓝 a) ↔ ∀ ε > (1 : α), ∀ᶠ b in x, |f b / a|ₘ < ε := by
  simp [nhds_eq_iInf_mabs_div, mabs_div_comm a]

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