mul_left

Mathlib.Topology.Algebra.InfiniteSum.Ring

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

English

If Summable f, then Summable (λ i, a * f(i)).

Русский

Если f суммируема, то и последовательность a · f(i) суммируема.

LaTeX

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

Lean4

theorem mul_left (a) (hf : Summable f L) : Summable (fun i ↦ a * f i) L :=
  (hf.hasSum.mul_left _).summable

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

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

Разделы

Аффилиация

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