tendsto_nhds_of_eventually_eq — Mathlib

English

If f is eventually equal to a constant x along a filter l, then f tends to x in nhds x.

Русский

Если функция f стремится к константе x по фильтру l в смысле равенства, то f сходится к x в nhds x.

LaTeX

$$$\\text{Tendsto } f\\ l\\ (\\mathcal{N} x) \\text{ если } (\\forall^* a'\\in l, f(a')=x).$$$

Lean4

theorem tendsto_nhds_of_eventually_eq {l : Filter α} {f : α → X} (h : ∀ᶠ x' in l, f x' = x) : Tendsto f l (𝓝 x) :=
  tendsto_const_nhds.congr' (.symm h)

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