of_subsingleton_right — Mathlib

English

If β is a Subsingleton, then any f: α → β is EventuallyConst along any filter l.

Русский

Если β является подсинглетоном, то любая функция f: α → β является EventuallyConst вдоль любого фильтра l.

LaTeX

$$$[\text{Subsingleton}(\beta)] \Rightarrow \mathrm{EventuallyConst}(f,l)$$$

Lean4

@[nontriviality]
theorem of_subsingleton_right [Subsingleton β] : EventuallyConst f l :=
  .of_subsingleton

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