sum_apply — Mathlib

English

The sum of multilinear maps evaluated at a fixed vector equals the sum of their evaluations; a special case of the above sum rules.

Русский

Сумма мультилейных отображений, применённых к фиксированному вектору, равна сумме их значений; частный случай вышеуказанных правил суммирования.

LaTeX

$$$\forall f: \alpha \to MultilinearMap R M_1 M_2, \forall s: Finset \alpha,\; \big(\sum_{a\in s} f(a)\big)(m) = \sum_{a\in s} f(a)(m)$$$

Lean4

theorem sum_apply {α : Type*} (f : α → MultilinearMap R M₁ M₂) (m : ∀ i, M₁ i) {s : Finset α} :
    (∑ a ∈ s, f a) m = ∑ a ∈ s, f a m := by simp

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