tsum_mul_left — Mathlib

English

In a suitable topological real setting, ∑' i, a * f i = a * ∑' i, f i.

Русский

В подходящей топологической среде над числами, сумма a · f(i) равна a умноженному на сумму f(i).

LaTeX

$$$[T2Space \alpha] \Rightarrow \sum' i, a \cdot f(i) = a \cdot \sum' i, f(i)$$$

Lean4

theorem tsum_mul_left [T2Space α] : ∑'[L] x, a * f x = a * ∑'[L] x, f x :=
  by
  by_cases ha : a = 0
  · simp [ha]
  · exact ((Homeomorph.mulLeft₀ a ha).isClosedEmbedding.map_tsum f (g := AddMonoidHom.mulLeft a)).symm

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