ker_closedComplemented_of_finiteDimensional_range

English

If a continuous linear map has finite-dimensional range, then its kernel is complemented by a closed subspace; i.e., ker f has a closed complement in E.

Русский

Если образ конечной размерности, то ядро отображения имеет закрытое дополнение в E.

LaTeX

$$$$(\ker f) \text{ is ClosedComplemented in } E.$$$$

Lean4

theorem ker_closedComplemented_of_finiteDimensional_range (f : E →L[𝕜] F) [FiniteDimensional 𝕜 (range f)] :
    (ker f).ClosedComplemented :=
  by
  set f' : E →L[𝕜] range f := f.codRestrict _ (LinearMap.mem_range_self (f : E →ₗ[𝕜] F))
  rcases f'.exists_right_inverse_of_surjective (f : E →ₗ[𝕜] F).range_rangeRestrict with ⟨g, hg⟩
  simpa only [f', ker_codRestrict] using f'.closedComplemented_ker_of_rightInverse g (ContinuousLinearMap.ext_iff.1 hg)

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