tendsto_nhds_of_Icc — Mathlib

English

If for every ε>0 the image of a net eventually lies in Icc(a−ε, a+ε), then the net converges to a.

Русский

Если для каждого ε>0 образ сетки в итоге лежит в Icc(a−ε, a+ε), то сетка сходится к a.

LaTeX

$$For all ε>0, eventually in f x ∈ Icc(a−ε, a+ε) implies Tendsto f to a$$

Lean4

protected theorem tendsto_nhds_of_Icc {f : Filter α} {u : α → ℝ≥0∞} {a : ℝ≥0∞}
    (h : ∀ ε > 0, ∀ᶠ x in f, u x ∈ Icc (a - ε) (a + ε)) : Tendsto u f (𝓝 a) :=
  by
  refine Tendsto.mono_right ?_ (biInf_le_nhds _)
  simpa only [tendsto_iInf, tendsto_principal]

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