lsub_const

Mathlib.SetTheory.Ordinal.Family

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

English

If I is nonempty and o is an ordinal, then the lsub of the constant function to o equals succ(o).

Русский

Пусть I непустое и o — ординал. Тогда lsub(constant to o) = succ(o).

LaTeX

$$$\operatorname{lsub}(\lambda_{\_}:I.\! o) = \operatorname{succ}(o)$$$

Lean4

@[simp]
theorem lsub_const {ι} [Nonempty ι] (o : Ordinal) : (lsub fun _ : ι => o) = succ o :=
  ciSup_const

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

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

Разделы

Аффилиация

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