card_sInf_range_compl_le — Mathlib

English

The non-lifted version: the cardinality bound for the infimum of the complement of the range of f.

Русский

Не взведенная версия: ограничение кардинальности infimum дополнения range f.

LaTeX

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

Lean4

theorem card_sInf_range_compl_le {ι : Type u} (f : ι → Ordinal.{u}) : (sInf (range f)ᶜ).card ≤ #ι :=
  Cardinal.lift_id #ι ▸ card_sInf_range_compl_le_lift f

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