map_add_univ — Mathlib

English

For a continuous multilinear map f on Fin(n+1) spaces, f(m+m') equals the sum over all subsets s of ι of f(s.piecewise m m').

Русский

Для отображения мультилейнного типа с пространствами Fin(n+1) выполняется: f(m+m') = ∑_{s⊆ι} f(s.piecewise m m').

LaTeX

$$$f(m+m') = \sum_{s \subseteq \iota} f\bigl(s.piecewise(m,m')\bigr).$$$

Lean4

/-- Additivity of a continuous multilinear map along all coordinates at the same time,
writing `f (m + m')` as the sum of `f (s.piecewise m m')` over all sets `s`. -/
theorem map_add_univ [DecidableEq ι] [Fintype ι] (m m' : ∀ i, M₁ i) :
    f (m + m') = ∑ s : Finset ι, f (s.piecewise m m') :=
  f.toMultilinearMap.map_add_univ _ _

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