lsub_le_iff

Mathlib.SetTheory.Ordinal.Family

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

English

lsub f ≤ a if and only if for every i, f i < a.

Русский

lsub f ≤ a эквивалентно ∀ i, f i < a.

LaTeX

$$$\\, lsub f \\le a \\iff \\forall i, f(i) < a$$$

Lean4

theorem lsub_le_iff {ι} {f : ι → Ordinal} {a} : lsub f ≤ a ↔ ∀ i, f i < a := by
  simpa using Ordinal.iSup_le_iff (f := succ ∘ f)

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

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

Разделы

Аффилиация

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