of_norm

Mathlib.Analysis.Normed.Group.InfiniteSum

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

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_norm {f : ι → E} (hf : Summable fun a => ‖f a‖) : Summable f :=
  .of_norm_bounded hf fun _i => le_rfl

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

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

Разделы

Аффилиация

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