sum_eq_iSup_lift — Mathlib

English

If hι: ℵ0 ≤ #ι and h: lift(#ι) ≤ iSup f, then sum f = iSup f.

Русский

Если hι: ℵ0 ≤ |ι| и h: lift(|ι|) ≤ iSup f, тогда сумма \sum f равна iSup f.

LaTeX

$$$\forall f: I \to \mathrm{Cardinal},\ (\text{lift} \, \lvert I\rvert \le \iSup f) \land (\aleph_0 \le \lvert I\rvert) \Rightarrow \sum f = \iSup f$$$

Lean4

theorem sum_eq_iSup_lift {f : ι → Cardinal.{max u v}} (hι : ℵ₀ ≤ #ι) (h : lift.{v} #ι ≤ iSup f) : sum f = iSup f :=
  by
  apply (iSup_le_sum f).antisymm'
  convert sum_le_iSup_lift f
  rw [mul_eq_max (aleph0_le_lift.mpr hι) ((aleph0_le_lift.mpr hι).trans h), max_eq_right h]

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