blsub_id

Mathlib.SetTheory.Ordinal.Family

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

English

Bsup over succ o of the identity equals o.

Русский

Bsup над succ o от идентитета даёт o.

LaTeX

$$$ \\operatorname{bsup}(\\operatorname{succ}(o),\\lambda x\\_,x) = o $$$

Lean4

@[simp]
theorem blsub_id : ∀ o, (blsub.{u, u} o fun x _ => x) = o :=
  lsub_typein

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

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

Разделы

Аффилиация

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