lt_blsub

Mathlib.SetTheory.Ordinal.Family

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

English

For any o, any f : a < o → Ordinal, and any i with i < o, f(i,i<o) < blsub(o,f).

Русский

Для любого o, любой f: {a<o} → Ordinal и любого i < o, выполнено f(i,i<o) < blsub(o,f).

LaTeX

$$$\forall o : \mathrm{Ordinal},\ \forall f : \forall a < o, \mathrm{Ordinal},\forall i,\forall h,\ f(i,h) < \mathrm{blsub}(o,f)$$$

Lean4

theorem lt_blsub {o} (f : ∀ a < o, Ordinal) (i h) : f i h < blsub o f :=
  blsub_le_iff.1 le_rfl _ _

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

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

Разделы

Аффилиация

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