card_iSup_Iio_le_sum_card — Mathlib

English

Let o be an ordinal and f its restriction to Iio(o). Then the cardinal of the supremum over Iio(o) is ≤ the sum of cardinals of f(a).

Русский

Пусть o — ординал и f ограничено до Iio(o). Тогда card( sup_{a∈Iio(o)} f(a) ) ≤ ∑_{a∈Iio(o)} card(f(a)).

LaTeX

$$\#(\bigsup_{a∈Iio(o)} f(a)) ≤ \sum_{i} (f((enumIsoToType o).symm i).card)$$

Lean4

theorem card_iSup_Iio_le_sum_card {o : Ordinal.{u}} (f : Iio o → Ordinal.{max u v}) :
    (⨆ a : Iio o, f a).card ≤ Cardinal.sum fun i ↦ (f ((enumIsoToType o).symm i)).card :=
  by
  apply le_of_eq_of_le (congr_arg _ _).symm (card_iSup_le_sum_card _)
  simpa using (enumIsoToType o).symm.iSup_comp (g := fun x ↦ f x)

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