blsub_const

Mathlib.SetTheory.Ordinal.Family

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

English

If o ≠ 0, then blsub o (constant a) = succ a.

Русский

Если o ≠ 0, то blsub o (константа a) = succ a.

LaTeX

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

Lean4

theorem blsub_const {o : Ordinal} (ho : o ≠ 0) (a : Ordinal) : (blsub.{u, v} o fun _ _ => a) = succ a :=
  bsup_const.{u, v} ho (succ a)

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

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

Разделы

Аффилиация

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