English
If a bounded linear bijection between normed spaces is continuous, its inverse is also continuous (Banach open mapping theorem).
Русский
Пусть ограниченное линейное биективное отображение между нормированными пространствами непрерывно. Тогда его обратное отображение также непрерывно (теорема открытого отображения Банаха).
LaTeX
$$$\\text{If } e: E \\to F \\text{ is a bijective bounded linear map and continuous, then } e^{-1} \\text{ is continuous.}$$$
Lean4
/-- An injective continuous linear map with a closed range defines a continuous linear equivalence
between its domain and its range. -/
noncomputable def equivRange (hinj : Injective f) (hclo : IsClosed (range f)) : E ≃SL[σ] LinearMap.range f :=
have : CompleteSpace (LinearMap.range f) := hclo.completeSpace_coe
LinearEquiv.toContinuousLinearEquivOfContinuous (LinearEquiv.ofInjective f.toLinearMap hinj) <|
(f.continuous.codRestrict fun x ↦ LinearMap.mem_range_self f x).congr fun _ ↦ rfl
