English
Surjective continuous linear maps between Banach spaces are quotient maps and hence open onto their images.
Русский
Сюръективные непрерывно линейные отображения между банаховыми пространствами являются фактор-отображениями и следовательно открыты относительно их образов.
LaTeX
$$$$\\text{IsQuotientMap}(f)$$$$
Lean4
theorem _root_.AffineMap.isOpenMap {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {P Q : Type*}
[MetricSpace P] [NormedAddTorsor E P] [MetricSpace Q] [NormedAddTorsor F Q] (f : P →ᵃ[𝕜] Q) (hf : Continuous f)
(surj : Surjective f) : IsOpenMap f :=
AffineMap.isOpenMap_linear_iff.mp <|
ContinuousLinearMap.isOpenMap { f.linear with cont := AffineMap.continuous_linear_iff.mpr hf }
(f.linear_surjective_iff.mpr surj)
