theorem OpenMapping.open_mapping_theorem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [CompleteSpace V] {W : Type u_3} [NormedAddCommGroup W] [NormedSpace 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) (hT : Function.Surjective ⇑T) : IsOpenMap ⇑T

Open Mapping Theorem. Let $B_1, B_2$ be two Banach spaces, and let $T \in \mathcal{B}(B_1, B_2)$ be a surjective bounded linear operator. Then $T$ is an open map, meaning that for every open subset $U \subset B_1$, the image $T(U)$ is open in $B_2$.

noncomputable def OpenMapping.continuousLinearEquivOfBijective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [CompleteSpace V] {W : Type u_3} [NormedAddCommGroup W] [NormedSpace 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) (hT : Function.Bijective ⇑T) : V ≃L[𝕜] W

The continuous linear equivalence $V \simeq_L W$ constructed from a bijective bounded linear operator $T : V \to W$ between Banach spaces. By the Open Mapping Theorem, the set-theoretic inverse is automatically continuous, so $T$ upgrades to a continuous linear equivalence.

theorem OpenMapping.bijective_bounded_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace 𝕜 V] [CompleteSpace V] {W : Type u_3} [NormedAddCommGroup W] [NormedSpace 𝕜 W] [CompleteSpace W] (T : V →L[𝕜] W) (hT : Function.Bijective ⇑T) : ∃ (S : W →L[𝕜] V), (∀ (w : W), T (S w) = w) ∧ ∀ (v : V), S (T v) = v

Bounded Inverse Theorem (Corollary of the Open Mapping Theorem). If $B_1, B_2$ are two Banach spaces and $T \in \mathcal{B}(B_1, B_2)$ is bijective, then there exists a bounded linear operator $S : B_2 \to B_1$ which is a two-sided inverse of $T$, i.e. $T \circ S = \mathrm{id}_{B_2}$ and $S \circ T = \mathrm{id}_{B_1}$. In particular, $T^{-1} \in \mathcal{B}(B_2, B_1)$.