bsup_const

Mathlib.SetTheory.Ordinal.Family

URI: https://scilib.ai/kg/mathlib#Ordinal.bsup_const

← MathLib Explorer

English

If o ≠ 0, bsup o of a constant value a returns a.

Русский

Если o не нулевой, bsup o константы a равен a.

LaTeX

$$$o \\neq 0 \\Rightarrow \\operatorname{bsup}(o, (\\lambda\\_,\\_=>a)) = a$$$

Lean4

theorem bsup_const {o : Ordinal.{u}} (ho : o ≠ 0) (a : Ordinal.{max u v}) : (bsup.{_, v} o fun _ _ => a) = a :=
  le_antisymm (bsup_le fun _ _ => le_rfl) (le_bsup _ 0 (Ordinal.pos_iff_ne_zero.2 ho))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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