bsup_id_limit

Mathlib.SetTheory.Ordinal.Family

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

English

If every successor of a is below o, then bsup o (id) = o.

Русский

Если для всех a < o выполняется a+1 < o, то bsup o(id) = o.

LaTeX

$$$ (\\forall a < o)\, (\\operatorname{succ}(a) < o) \\Rightarrow \\operatorname{bsup}(o,\\lambda x\\_,x) = o $$$

Lean4

theorem bsup_id_limit {o : Ordinal} : (∀ a < o, succ a < o) → (bsup.{u, u} o fun x _ => x) = o :=
  iSup_typein_limit

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

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

Разделы

Аффилиация

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