Banach open mapping theorem
This file contains the Banach open mapping theorem, i.e., the fact that a bijective bounded linear map between Banach spaces has a bounded inverse.
First step of the proof of the Banach open mapping theorem (using completeness of F):
by Baire's theorem, there exists a ball in E whose image closure has nonempty interior.
Rescaling everything, it follows that any y ∈ F is arbitrarily well approached by
images of elements of norm at most C * ∥y∥.
For further use, we will only need such an element whose image
is within distance ∥y∥/2 of y, to apply an iterative process.
The Banach open mapping theorem: if a bounded linear map between Banach spaces is onto, then any point has a preimage with controlled norm.
The Banach open mapping theorem: a surjective bounded linear map between Banach spaces is open.
If a bounded linear map is a bijection, then its inverse is also a bounded linear map.
Associating to a linear equivalence between Banach spaces a continuous linear equivalence when the direct map is continuous, thanks to the Banach open mapping theorem that ensures that the inverse map is also continuous.
Equations
- e.to_continuous_linear_equiv_of_continuous h = {to_linear_equiv := {to_fun := e.to_fun, map_add' := _, map_smul' := _, inv_fun := e.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := h, continuous_inv_fun := _}
Convert a bijective continuous linear map f : E →L[𝕜] F between two Banach spaces
to a continuous linear equivalence.
Equations
- continuous_linear_equiv.of_bijective f hinj hsurj = (linear_equiv.of_bijective ↑f hinj hsurj).to_continuous_linear_equiv_of_continuous _