of_tendsto — Mathlib

English

If f tends to a constant x along l, then f is eventually constant along l.

Русский

Если f стремится к константе x вдоль фильтра l, тогда f становится константной вдоль l.

LaTeX

$$$\\\\forall {f} {l} {x},\\\\; (\\\\text{Tendsto } f l (\\\\text{pure } x)) \\\\Rightarrow \\\\text{EventuallyConst } f l$$$

Lean4

theorem of_tendsto {x : β} (h : Tendsto f l (pure x)) : EventuallyConst f l :=
  have : Nonempty β := ⟨x⟩;
  eventuallyConst_iff_tendsto.2 ⟨x, h⟩

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