of_subsingleton_left

Mathlib.Order.Filter.EventuallyConst

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyConst.of_subsingleton_left

English

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

Русский

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

LaTeX

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

Lean4

@[nontriviality]
theorem of_subsingleton_left [Subsingleton α] : EventuallyConst f l :=
  .map .of_subsingleton f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru