map_add_univ — Mathlib

English

For a finite index ι and a continuous alternating map f, the sum over all coordinate contributions equals the evaluation on the sum of the arguments across all coordinates.

Русский

Для конечного множества индексов ι и непрерывной чередующей карты f сумма по всем координатам даёт значение, полученное на сумме аргументов по всем координатам.

LaTeX

$$$f( m + m' ) = \sum_{s \subseteq ι} f( s.piecewise m m' ).$$$

Lean4

/-- Additivity of a continuous alternating 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' : ι → M) : f (m + m') = ∑ s : Finset ι, f (s.piecewise m m') :=
  f.toMultilinearMap.map_add_univ _ _

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