card_iSup_le_sum_card — Mathlib

English

For a family of ordinals f(i), the inequality holds: (iSup_i f(i)).card ≤ sum_i (f(i)).card.

Русский

Для семейства ординалов f(i) выполняется: (iSup_i f(i)).card ≤ ∑_i (f(i)).card.

LaTeX

$$(\bigsup_i f(i)).card \le \sum_i (f(i)).card$$

Lean4

theorem card_iSup_le_sum_card {ι : Type u} (f : ι → Ordinal.{max u v}) :
    (⨆ i, f i).card ≤ Cardinal.sum (fun i ↦ (f i).card) :=
  by
  have := lift_card_iSup_le_sum_card f
  rwa [Cardinal.lift_id'] at this

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