decompose_sum — Mathlib

English

For a family ℳ, the symm of the decomposition distributes over a finite sum: (decompose ℳ).symm (∑ f i) = ∑ (decompose ℳ).symm (f i).

Русский

Обратная к декомпозиции по ℳ распределяет по конечной сумме: (decompose ℳ).symm (∑ f i) = ∑ (decompose ℳ).symm (f i).

LaTeX

$$$\big(\mathrm{decompose}_{\mathcal{M}}\big)^{-1}\Big(\sum_{i\in s} f_i\Big) = \sum_{i\in s} \big(\mathrm{decompose}_{\mathcal{M}}\big)^{-1}(f_i)$$$

Lean4

@[simp]
theorem decompose_sum {ι'} (s : Finset ι') (f : ι' → M) : decompose ℳ (∑ i ∈ s, f i) = ∑ i ∈ s, decompose ℳ (f i) :=
  map_sum (decomposeAddEquiv ℳ) f s

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