English
For a small index set, the lifted supremum of a family of ordinals has cardinal ≤ the sum of the cardinals of the family.
Русский
Для малого множества индексов верхняя граница по Лифт-определению суммарная по кардиналам членов семьи.
LaTeX
$$\operatorname{lift}((\bigsup_i f(i)).card) \le \sum_i (f(i)).card$$
Lean4
theorem lift_card_iSup_le_sum_card {ι : Type u} [Small.{v} ι] (f : ι → Ordinal.{v}) :
Cardinal.lift.{u} (⨆ i, f i).card ≤ Cardinal.sum fun i ↦ (f i).card :=
by
simp_rw [← mk_toType]
rw [← mk_sigma, ← Cardinal.lift_id'.{v} #(Σ _, _), ← Cardinal.lift_umax.{v, u}]
apply
lift_mk_le_lift_mk_of_surjective (f :=
enumIsoToType _ ∘
(⟨(enumIsoToType _).symm ·.2, (mem_Iio.mp ((enumIsoToType _).symm _).2).trans_le (Ordinal.le_iSup _ _)⟩))
rw [EquivLike.comp_surjective]
rintro ⟨x, hx⟩
obtain ⟨i, hi⟩ := Ordinal.lt_iSup_iff.mp hx
exact ⟨⟨i, enumIsoToType _ ⟨x, hi⟩⟩, by simp⟩
