eventuallyConst_iff_exists_eventuallyEq

English

A repeated variant: there exists c such that f equals c eventually along the filter.

Русский

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

LaTeX

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

Lean4

theorem eventuallyConst_iff_exists_eventuallyEq [Nonempty β] : EventuallyConst f l ↔ ∃ c, f =ᶠ[l] fun _ ↦ c :=
  subsingleton_iff_exists_singleton_mem

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