iSup_le_lsub

Mathlib.SetTheory.Ordinal.Family

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

English

iSup f ≤ lsub f for any f.

Русский

iSup f ≤ lsub f для любого f.

LaTeX

$$$iSup f \\le lsub f$$$

Lean4

theorem iSup_le_lsub {ι} (f : ι → Ordinal) : iSup f ≤ lsub f :=
  Ordinal.iSup_le fun i => (lt_lsub f i).le

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

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

Разделы

Аффилиация

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