English
If f is a continuous alternating map and g' a family of functions indexed by i with finite index sets A i, then the sum over universal indices equals the piFinset sum over all selectors r of f applied to g' with r_i selections.
Русский
Если f — непрерывная чередующая карта и g' — семейство функций с индексируемыми конечными множествами A_i, то сумма по всем индексам равна сумме по всем выборкам r над f, примененной к g'(r_i).
LaTeX
$$$ (\forall i, A_i )\ (f) \ncong (\piFinset A).$$$
Lean4
/-- If `f` is continuous alternating, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the
sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ...,
`r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each
coordinate. -/
theorem map_sum_finset : (f fun i => ∑ j ∈ A i, g' i j) = ∑ r ∈ piFinset A, f fun i => g' i (r i) :=
f.toMultilinearMap.map_sum_finset _ _
