sInf_compl_lt_ord_succ — Mathlib

English

The infimum of the complement of the range of a family is strictly less than the ordinals of the successor of the index cardinal.

Русский

Нижняя граница дополнения диапазона семейства строго меньше ординала следующего кардинала индекса.

LaTeX

$$$$ \\operatorname{sInf}(\\operatorname{range}(f))^{c} < (\\operatorname{succ}(\\#\\iota)).\\operatorname{ord} $$$$

Lean4

theorem sInf_compl_lt_ord_succ {ι : Type u} (f : ι → Ordinal.{u}) : sInf (range f)ᶜ < (succ #ι).ord :=
  lift_id (succ #ι).ord ▸ sInf_compl_lt_lift_ord_succ f

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