of_nnnorm

Mathlib.Analysis.Normed.Group.InfiniteSum

URI: https://scilib.ai/kg/mathlib#Summable.of_nnnorm

English

If ∑ ‖f i‖₊ converges, then ∑ f i converges.

Русский

Если ∑ ‖f_i‖₊ сходится, то ∑ f_i сходится.

LaTeX

$$$\\text{Summable }(\\|f i\\|_+) \\Rightarrow \\text{Summable } f$$$

Lean4

theorem of_nnnorm {f : ι → E} (hf : Summable fun a => ‖f a‖₊) : Summable f :=
  .of_nnnorm_bounded hf fun _i => le_rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru