const_smul

Mathlib.Topology.Algebra.InfiniteSum.Module

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

English

If f is Summable, then the constant-scaled sequence b • f is Summable.

Русский

Если f суммируема, то последовательность b • f суммируема.

LaTeX

$$$$ \text{Summable } f L \Rightarrow \text{Summable } (\lambda i, b \cdot f i) L. $$$$

Lean4

theorem const_smul (b : γ) (hf : Summable f L) : Summable (fun i ↦ b • f i) L :=
  (hf.hasSum.const_smul _).summable

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

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

Разделы

Аффилиация

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