English
There is a canonical linear equivalence between the family of maps indexed by ι' into continuous alternating maps and the dependent map into M' i, generalizing the previous pi-equivalence.
Русский
Существует каноническое линейное эквивалентное отображение между семейством отображений, индексируемых ι', в непрерывные чередующие отображения и зависимое отображение в M' i, обобщающее предыдущее Pi-эквивалентность.
LaTeX
$$$$ \\text{piLinearEquiv} : (\\forall i, \\; M [⋀^ι]→L[A] M' i) \\simeq_{R} M [⋀^ι]→L[A] \\forall i, M' i. $$$$
Lean4
/-- `ContinuousLinearMap.compContinuousAlternatingMap` as a bundled bilinear map. -/
def _root_.ContinuousLinearMap.compContinuousAlternatingMapₗ :
(N →L[R] N') →ₗ[R] (M [⋀^ι]→L[R] N) →ₗ[R] (M [⋀^ι]→L[R] N') :=
LinearMap.mk₂ R ContinuousLinearMap.compContinuousAlternatingMap (fun _ _ _ => rfl) (fun _ _ _ => rfl)
(fun f g₁ g₂ => by ext1; apply f.map_add) fun c f g => by ext1; simp
