card_sInf_range_compl_le_lift — Mathlib

English

For any index type ι and f : ι → Ordinal, the infimum cardinal of the complement of the range is bounded by the lifted cardinal of ι.

Русский

Для любого индекса ι и f: ι → Ordinal нижняя граница дополнения множества range f ограничена взведенной кардинальностью ι.

LaTeX

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

Lean4

theorem card_sInf_range_compl_le_lift {ι : Type u} (f : ι → Ordinal.{max u v}) :
    (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v} #ι :=
  by
  rw [← Cardinal.lift_le.{max u v + 1}, Cardinal.lift_lift]
  apply (lift_card_sInf_compl_le _).trans
  rw [← Cardinal.lift_id'.{u, max u v + 1} #(range _)]
  exact mk_range_le_lift

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