summable_mul_left_iff — Mathlib

English

If a ≠ 0, Summable (λ i, a * f i) L ⇔ Summable f L.

Русский

Для a ≠ 0, суммируема ли последовательность a · f(i) ⇔ суммируема сама f(i).

LaTeX

$$$(\forall a, a \neq 0) \ Rightarrow \left( \text{Summable } (\lambda i, a \cdot f(i)) L \iff \text{Summable } f L \right)$$$

Lean4

theorem summable_mul_left_iff (h : a ≠ 0) : (Summable (fun i ↦ a * f i) L) ↔ Summable f L :=
  ⟨fun H ↦ by simpa only [inv_mul_cancel_left₀ h] using H.mul_left a⁻¹, fun H ↦ H.mul_left _⟩

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