English
In the Fin(n+1)-indexed setting, a continuous multilinear map is additive in the first variable: f(cons(x+y,m)) = f(cons(x,m)) + f(cons(y,m)).
Русский
В случае индексации Fin(n+1) отображение непрерывно мультилинейно по первой переменной и удовлетворяет аддитивности: f(cons(x+y,m)) = f(cons(x,m)) + f(cons(y,m)).
LaTeX
$$$f(\mathrm{cons}(x+y,m)) = f(\mathrm{cons}(x,m)) + f(\mathrm{cons}(y,m)).$$$
Lean4
/-- In the specific case of continuous multilinear maps on spaces indexed by `Fin (n+1)`, where one
can build an element of `(i : Fin (n+1)) → M i` using `cons`, one can express directly the
additivity of a multilinear map along the first variable. -/
theorem cons_add (f : ContinuousMultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (x y : M 0) :
f (cons (x + y) m) = f (cons x m) + f (cons y m) :=
f.toMultilinearMap.cons_add m x y
