sum_lt_lift_of_isRegular — Mathlib

English

Let c be a regular cardinal and hι: lift(#ι) < c. If every f(i) < c, then sum f < c.

Русский

Пусть c — регулярное кардинальное число и hι: lift(#ι) < c. Если для всех i f(i) < c, то сумма sum f < c.

LaTeX

$$$IsRegular(c) \land \operatorname{lift}(\#ι) < c \Rightarrow ( \forall i, f(i) < c ) \Rightarrow \operatorname{sum}(f) < c$$$

Lean4

theorem sum_lt_lift_of_isRegular {ι : Type u} {f : ι → Cardinal} {c : Cardinal} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} #ι < c) (hf : ∀ i, f i < c) : sum f < c :=
  (sum_le_iSup_lift _).trans_lt <| mul_lt_of_lt hc.1 hι (iSup_lt_lift_of_isRegular hc hι hf)

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