lt_lsub

Mathlib.SetTheory.Ordinal.Family

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

English

For any i, f(i) < lsub f; i.e., each component is below the lsub.

Русский

Для любого i имеет место f(i) < lsub f; каждый элемент ниже lsub.

LaTeX

$$$f(i) < lsub f$$$

Lean4

theorem lt_lsub {ι} (f : ι → Ordinal) (i) : f i < lsub f :=
  succ_le_iff.1 (Ordinal.le_iSup _ i)

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

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

Разделы

Аффилиация

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