English
Symmetry of congruence left-right in continuous linear equivalences yields equalities with inverses.
Русский
Симметрия в теоремах о конгруэнтности слева и справа для непрерывных линейных эквивалентностей приводит к равенствам с обратными.
LaTeX
$$$ (g.continuousAlternatingMapCongrRight).symm = g^{-1}.continuousAlternatingMapCongrRight $$$
Lean4
/-- Given a continuous linear isomorphism between the domains,
generate a continuous linear isomorphism between the spaces of continuous alternating maps.
This is `ContinuousAlternatingMap.compContinuousLinearMap` as an equivalence,
and is the continuous version of `AlternatingMap.domLCongr`. -/
@[simps apply]
def continuousAlternatingMapCongrLeft (f : E ≃L[𝕜] F) : E [⋀^ι]→L[𝕜] G ≃L[𝕜] (F [⋀^ι]→L[𝕜] G)
where
__ := f.continuousAlternatingMapCongrLeftEquiv
__ := ContinuousAlternatingMap.compContinuousLinearMapCLM (f.symm : F →L[𝕜] E)
toFun g := g.compContinuousLinearMap (f.symm : F →L[𝕜] E)
continuous_invFun := (ContinuousAlternatingMap.compContinuousLinearMapCLM (f : E →L[𝕜] F)).cont
continuous_toFun := (ContinuousAlternatingMap.compContinuousLinearMapCLM (f.symm : F →L[𝕜] E)).cont
