English
The product of two spaces of continuous alternating maps is isometric to the space of alternating maps into the product space.
Русский
Произведение двух пространств непрерывных чередующихся отображений изометрично в пространство чередующихся отображений в произведении пространств.
LaTeX
$$$ (f_1,f_2) \mapsto f_1.\mathrm{prod} f_2 $ induces a LinearIsometryEquiv$\,$ between $(E [⋀^ι]→L[𝕜] F) × (E [⋀^ι]→L[𝕜] G)$ and $E [⋀^ι]→L[𝕜] (F \times G)$$$
Lean4
/-- `ContinuousAlternatingMap.prod` as a `LinearIsometryEquiv`. -/
@[simps]
def prodLIE : (E [⋀^ι]→L[𝕜] F) × (E [⋀^ι]→L[𝕜] G) ≃ₗᵢ[𝕜] (E [⋀^ι]→L[𝕜] (F × G))
where
toFun f := f.1.prod f.2
invFun
f :=
((ContinuousLinearMap.fst 𝕜 F G).compContinuousAlternatingMap f,
(ContinuousLinearMap.snd 𝕜 F G).compContinuousAlternatingMap f)
map_add' _ _ := rfl
map_smul' _ _ := rfl
norm_map' f := opNorm_prod f.1 f.2
