exists_right_inverse_of_surjective

English

If a continuous linear map f: E → F is surjective and F is finite-dimensional, then there exists g: F → E with f ∘ g = id_F.

Русский

Если линейное отображение f: E → F сюръективно и F конечномерно, существует g: F → E такое, что f ∘ g = id_F.

LaTeX

$$$\\exists g: F \\to_L[𝕜] E \\;\\text{ such that }\\; f \\circ g = \\mathrm{id}_{F}$$$

Lean4

theorem exists_right_inverse_of_surjective [FiniteDimensional 𝕜 F] (f : E →L[𝕜] F) (hf : LinearMap.range f = ⊤) :
    ∃ g : F →L[𝕜] E, f.comp g = ContinuousLinearMap.id 𝕜 F :=
  let ⟨g, hg⟩ := (f : E →ₗ[𝕜] F).exists_rightInverse_of_surjective hf
  ⟨LinearMap.toContinuousLinearMap g, ContinuousLinearMap.coe_inj.1 hg⟩

Похожие утверждения