sum_lt_of_isRegular — Mathlib

English

If c is regular and #ι < c, and each f(i) < c, then sum f < c.

Русский

Если c регулярное и #ι < c, и каждый f(i) < c, то сумма f меньше c.

LaTeX

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

Lean4

theorem sum_lt_of_isRegular {ι : Type u} {f : ι → Cardinal} {c : Cardinal} (hc : IsRegular c) (hι : #ι < c) :
    (∀ i, f i < c) → sum f < c :=
  sum_lt_lift_of_isRegular.{u, u} hc (by rwa [lift_id])

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