English
For spaces indexed by Fin (n+1), the vecCons and projection structure yield a bijection between the space of continuous alternating maps on a product and the product of maps; i.e., a Pi-equivalence for vecCons.
Русский
Для индексации Fin (n+1) структура vecCons и проекции дают биекцию между пространством непрерывных чередующих карт на произведение и произведением карт; тождество Пи-эквивалентности для vecCons.
LaTeX
$$$\text{Equiv}(\{\text{ContinuousAlternatingMap }R\ M\ N_i\}_{i},\text{ContinuousAlternatingMap }R\ M\ (\{N_i\}_i) ).$$$
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
multiplicativity of an alternating map along the first variable. -/
theorem vecCons_smul (f : ContinuousAlternatingMap R M N (Fin (n + 1))) (m : Fin n → M) (c : R) (x : M) :
f (vecCons (c • x) m) = c • f (vecCons x m) :=
f.toMultilinearMap.cons_smul m c x
