sum_eq_iSup — Mathlib

English

Let f: I → Cardinal with I infinite (ℵ0 ≤ #I) and lift(#I) ≤ iSup f. Then sum f = iSup f.

Русский

Пусть f: I → Cardinal, где I бесконечно (ℵ0 ≤ |I|) и lift(|I|) ≤ iSup f. Тогда сумма f = iSup f.

LaTeX

$$$\forall f:\, I \to \mathrm{Cardinal},\ (\aleph_0 \le |I|) \rightarrow (\text{lift} \, |I| \le \iSup f) \rightarrow \sum f = \iSup f$$$

Lean4

theorem sum_eq_iSup {f : ι → Cardinal.{u}} (hι : ℵ₀ ≤ #ι) (h : #ι ≤ iSup f) : sum f = iSup f :=
  sum_eq_iSup_lift hι ((lift_id #ι).symm ▸ h)

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