English
Continuous linear equivalences induce a corresponding equivalence between spaces of continuous alternating maps.
Русский
Непрерывные линейные эквивалентности порождают соответствующее эквивалентное отображение между пространствами непрерывных чередующихся отображений.
LaTeX
$$$\text{continuousAlternatingMapCongrRight}$ is a linear isometry between the spaces of alternating maps$$
Lean4
/-- `ContinuousLinearMap.compContinuousAlternatingMap` as a bundled continuous linear equiv. -/
@[simps +simpRhs apply]
def _root_.ContinuousLinearEquiv.continuousAlternatingMapCongrRight (g : F ≃L[𝕜] G) :
(E [⋀^ι]→L[𝕜] F) ≃L[𝕜] (E [⋀^ι]→L[𝕜] G)
where
__ := g.continuousAlternatingMapCongrRightEquiv
__ := compContinuousAlternatingMapCLM 𝕜 E F G g.toContinuousLinearMap
continuous_toFun := (compContinuousAlternatingMapCLM 𝕜 E F G g.toContinuousLinearMap).continuous
continuous_invFun := (compContinuousAlternatingMapCLM 𝕜 E G F g.symm.toContinuousLinearMap).continuous
