le_bsup

Mathlib.SetTheory.Ordinal.Family

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

English

The non-lifted variant: a bound on the card of sInf(range f) complement by #ι.

Русский

Не взведенная версия: граница на(card) sInf(range f) дополнения через #ι.

LaTeX

$$$$ (\\operatorname{sInf}(\\operatorname{range}(f))^{c}).\\operatorname{card} \\le \\#ι $$$$

Lean4

theorem le_bsup {o} (f : ∀ a < o, Ordinal) (i h) : f i h ≤ bsup o f :=
  bsup_le_iff.1 le_rfl _ _

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

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

Разделы

Аффилиация

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