blsub_le

Mathlib.SetTheory.Ordinal.Family

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

English

Bsup dominates Blsub in the sense that o.bsup f ≥ o.blsub f, and equality holds in certain configurations.

Русский

Bsup доминирует над Blsub: o.bsup f ≥ o.blsub f; равенство может быть достигнуто в определённых случаях.

LaTeX

$$$(o).bsup\, f \ge (o).blsub\, f$$$

Lean4

theorem blsub_le {o : Ordinal} {f : ∀ b < o, Ordinal} {a} : (∀ i h, f i h < a) → blsub o f ≤ a :=
  blsub_le_iff.2

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

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

Разделы

Аффилиация

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