sInf_compl_lt_lift_ord_succ — Mathlib

English

The infimum of the complement of the range is strictly less than the ordinal of the successor of the cardinality of the index set.

Русский

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

LaTeX

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

Lean4

theorem sInf_compl_lt_lift_ord_succ {ι : Type u} (f : ι → Ordinal.{max u v}) :
    sInf (range f)ᶜ < lift.{v} (succ #ι).ord :=
  by
  rw [lift_ord, Cardinal.lift_succ, ← card_le_iff]
  exact card_sInf_range_compl_le_lift f

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