eventuallyConst_iff_tendsto — Mathlib

English

A function is eventually constant along a filter if and only if there exists a constant value c such that f equals c eventually along the filter.

Русский

Функция является константной вдоль фильтра тогда и только тогда, когда существует константа c, такая что f =ᶠ c по фильтру.

LaTeX

$$$\\\\forall {f : \\alpha \\to \\beta},\\\\; (\\\\text{EventuallyConst } f l) \\\\Leftrightarrow \\\\exists c, f =\\\\^l\\\\mathrm{\\text{EventuallyEq}}(\\\\lambda _ . c)$$$

Lean4

theorem eventuallyConst_iff_tendsto [Nonempty β] : EventuallyConst f l ↔ ∃ x, Tendsto f l (pure x) :=
  subsingleton_iff_exists_le_pure

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