English
Any continuous linear equivalence e: M ≃L[R] M2 is invertible as a continuous linear map.
Русский
Любое непрерывно-линейное эквивалентное отображение e: M ≃L[R] M2 является обратимым как непрерывно-линейное отображение.
LaTeX
$$$\text{IsInvertible}(e: M \to M_2)$$$
Lean4
/-- Introduce a function `inverse` from `M →L[R] M₂` to `M₂ →L[R] M`, which sends `f` to `f.symm` if
`f` is a continuous linear equivalence and to `0` otherwise. This definition is somewhat ad hoc,
but one needs a fully (rather than partially) defined inverse function for some purposes, including
for calculus. -/
noncomputable def inverse : (M →L[R] M₂) → M₂ →L[R] M := fun f =>
if h : f.IsInvertible then ((Classical.choose h).symm : M₂ →L[R] M) else 0
