sum_le_iSup_lift — Mathlib

English

For a family f : ι → Cardinal, sum f ≤ lift(#ι) · iSup f.

Русский

Для семейства f : ι → Cardinal сумма f не превосходит lift(#ι) · iSup f.

LaTeX

$$$\sum f \le \operatorname{lift}(\#\iota) \cdot iSup f$$$

Lean4

theorem sum_le_iSup_lift {ι : Type u} (f : ι → Cardinal.{max u v}) : sum f ≤ Cardinal.lift #ι * iSup f :=
  by
  rw [← (iSup f).lift_id, ← lift_umax, lift_umax.{max u v, u}, ← sum_const]
  exact sum_le_sum _ _ (le_ciSup <| bddAbove_of_small _)

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