card_iSup_Iio_le_card_mul_iSup — Mathlib

English

For a family f over Iio(o), the left-hand cardinal of the supremum is bounded by the product of o.card lifted and the supremum of the cardinals of f.

Русский

Для семейства f над Iio(o) левая граница по кардиналу ограничена произведением o.card (вверх) и supremum(card(f(a))).

LaTeX

$$(\sup_{a∈Iio(o)} f(a)).card ≤ (o.card).lift × (\sup_{a∈Iio(o)} (f(a)).card)$$

Lean4

theorem card_iSup_Iio_le_card_mul_iSup {o : Ordinal.{u}} (f : Iio o → Ordinal.{max u v}) :
    (⨆ a : Iio o, f a).card ≤ Cardinal.lift.{v} o.card * ⨆ a : Iio o, (f a).card :=
  by
  apply (card_iSup_Iio_le_sum_card f).trans
  convert ← sum_le_iSup_lift _
  · exact mk_toType o
  · exact (enumIsoToType o).symm.iSup_comp (g := fun x ↦ (f x).card)

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