lift_card_sInf_compl_le — Mathlib

English

For a set s of ordinals, the lifted cardinal of the infimum of its complement is bounded above by the cardinal of s.

Русский

Для множества ординалов s взводимая кардинальность нижней границы дополнения не превосходит кардинальность s.

LaTeX

$$$$ \\operatorname{lift}_{u+1}\\bigl( (\\operatorname{sInf}(s^{c}))\\operatorname{card} \\bigr) \\le \\#s $$$$

Lean4

theorem lift_card_sInf_compl_le (s : Set Ordinal.{u}) : Cardinal.lift.{u + 1} (sInf sᶜ).card ≤ #s :=
  by
  rw [← mk_Iio_ordinal]
  refine mk_le_mk_of_subset fun x (hx : x < _) ↦ ?_
  rw [← not_notMem]
  exact notMem_of_lt_csInf' hx

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