Surjective continuous linear maps onto a finite-dimensional space #
Surjectivity onto a finite-dimensional space is stable under small perturbations in the operator norm: the surjective maps form an open subset of the space of continuous linear maps. The source is an arbitrary seminormed space over a complete nontrivially normed field.
Mathlib records the companion fact that a surjective continuous linear map between Banach spaces
is an open map, in ContinuousLinearMap.isOpenMap; the openness proved here is openness of the
locus of such maps inside E →L[𝕜] F, not of any one of them.
Main results #
TauCeti.isOpen_setOf_surjective: surjectivity onto a finite-dimensional space is an open condition on continuous linear maps.
theorem
TauCeti.isOpen_setOf_surjective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[SeminormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[FiniteDimensional 𝕜 F]
:
Surjectivity onto a finite-dimensional space is an open condition on continuous linear maps.