bot

Mathlib.Order.Filter.EventuallyConst

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

English

Every function f: α → β is eventually constant with respect to the bottom filter on α.

Русский

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

LaTeX

$$$\forall f:\alpha\to\beta,\mathrm{EventuallyConst}(f,\bot)$$$

Lean4

@[simp]
protected theorem bot : EventuallyConst f ⊥ :=
  subsingleton_bot

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

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

Разделы

Аффилиация

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