summable_unop — Mathlib

English

The sum over op f equals the op of the sum: tsum (λ x, op (f x)) = op (tsum f).

Русский

Сумма над op f равна операции op над суммой: tsum (op f) = op (tsum f).

LaTeX

$$$\\operatorname{tsum}_{L} (\\lambda x, \\operatorname{op}(f x)) = \\operatorname{op}\\big( \\operatorname{tsum}_{L} f \\big)$$$

Lean4

theorem summable_unop {f : β → αᵐᵒᵖ} : (Summable (fun a ↦ unop (f a)) L) ↔ Summable f L :=
  ⟨Summable.op, Summable.unop⟩

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