tendsto — Mathlib

English

Let X be a topological space, l a filter on α, and f: α → X. If f is eventually equal to the constant map x along l, then f tends to x along l.

Русский

Пусть X — топологическое множество, l — фильтр на α, и f: α → X. Если f в пределе эквивалентна константе x по отношению к l, то f сходится к x по l.

LaTeX

$$$(\\exists A \\in l, \\forall a \\in A, f(a) = x) \\Rightarrow \\operatorname{Tendsto}(f, l, \\mathcal{N}(x))$$$

Lean4

theorem tendsto {l : Filter α} {f : α → X} (hf : f =ᶠ[l] fun _ ↦ x) : Tendsto f l (𝓝 x) :=
  tendsto_nhds_of_eventually_eq hf

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