linearCombination_apply_of_mem_supported

English

If a finitely supported l is supported on a finite set s, then linearCombination_R(v)(l) equals the finite sum over s: ∑ i∈s l(i) v(i).

Русский

Если опора конечной поддержки $l$ лежит в конечном наборе $s$, то линейная комбинация равна сумме по $s$: ∑_{i∈s} l(i) v(i).

LaTeX

$$$\\text{linearCombination}_R(v)(l) = \\displaystyle\\sum_{i\\in s} l(i) \\cdot v(i).$$$

Lean4

theorem linearCombination_apply_of_mem_supported {l : α →₀ R} {s : Finset α} (hs : l ∈ supported R R (↑s : Set α)) :
    linearCombination R v l = s.sum fun i => l i • v i :=
  Finset.sum_subset hs fun x _ hxg => show l x • v x = 0 by rw [notMem_support_iff.1 hxg, zero_smul]

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