bsup_id_succ

Mathlib.SetTheory.Ordinal.Family

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

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 bsup_id_succ (o) : (bsup.{u, u} (succ o) fun x _ => x) = o :=
  iSup_typein_succ

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

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

Разделы

Аффилиация

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