English
If f: E →SL[σ] F is a surjective continuous linear map between Banach spaces, there exists a nonlinear right inverse g: F → E such that f ∘ g = id_F. Moreover, such a right inverse can be chosen nontrivial (norm bounded away from zero).
Русский
Если отображение f: E →SL[σ] F является сюръективным непрерывным линейным отображением между банаховыми пространствами, существует нелинейное правое обратное g: F → E такое, что f ∘ g = id_F. При этом можно выбрать такое правое обратное не тривиальным по норме.
LaTeX
$$$\\exists g: F \\to E \\text{ с } f\\circ g = \\mathrm{id}_F \\quad \\text{и} \\quad g \\text{ является нелинейным правым обратным}$$$
Lean4
theorem exists_nonlinearRightInverse_of_surjective (f : E →SL[σ] F) (hsurj : LinearMap.range f = ⊤) :
∃ fsymm : NonlinearRightInverse f, 0 < fsymm.nnnorm :=
by
choose C hC fsymm h using exists_preimage_norm_le _ (LinearMap.range_eq_top.1 hsurj)
use {
toFun := fsymm
nnnorm := ⟨C, hC.lt.le⟩
bound' := fun y => (h y).2
right_inv' := fun y => (h y).1 }
exact hC
