English
Similarly, for vecCons indexing, additivity in the first variable holds: f(vecCons (x+y) m) = f(vecCons x m) + f(vecCons y m).
Русский
Аналогично в индексации vecCons, выполняется аддитивность по первой переменной: f(vecCons (x+y) m) = f(vecCons x m) + f(vecCons y m).
LaTeX
$$$f(\text{vecCons}(x+y, m)) = f(\text{vecCons}(x, m)) + f(\text{vecCons}(y, m)).$$$
Lean4
/-- In the specific case of continuous alternating 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 an alternating map along the first variable. -/
theorem vecCons_add (f : ContinuousAlternatingMap R M N (Fin (n + 1))) (m : Fin n → M) (x y : M) :
f (vecCons (x + y) m) = f (vecCons x m) + f (vecCons y m) :=
f.toMultilinearMap.cons_add m x y
