English
A continuous linear equivalence between codomains defines a bijection between spaces of continuous alternating maps by postcomposition with the equivalence.
Русский
Непрерывное линейное эквивалентное отображение между кодомом задаёт биективное соответствие между пространствами непрерывных чередующих карт посредством пост-композиции с эквивалентностью.
LaTeX
$$$\text{Let } e: N \simeq_L[R] N'.\ (M [⋀^ι]→L[R] N) \cong (M [⋀^ι]→L[R] N').$$$
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 cons_smul (f : ContinuousAlternatingMap R M N (Fin (n + 1))) (m : Fin n → M) (c : R) (x : M) :
f (Fin.cons (c • x) m) = c • f (Fin.cons x m) :=
f.toMultilinearMap.cons_smul m c x
