English
A finite-dimensional subspace p of a normed space over 𝕜 is ClosedComplemented; i.e., there exists a closed complement with a continuous projection.
Русский
Конечномерное подпространство p нормированного пространства является замкнуто дополненным: существует замкнутое дополнение и непрерывная проекция.
LaTeX
$$$ [FiniteDimensional 𝕜 p] \\Rightarrow p.ClosedComplemented$$
Lean4
/-- Corollary of the **Hahn-Banach theorem**: if `f : p → F` is a continuous linear map
from a submodule of a normed space `E` over `𝕜`, `𝕜 = ℝ` or `𝕜 = ℂ`,
with a finite-dimensional range, then `f` admits an extension to a continuous linear map `E → F`.
Note that contrary to the case `F = 𝕜`, see `exists_extension_norm_eq`,
we provide no estimates on the norm of the extension.
-/
theorem exist_extension_of_finiteDimensional_range {p : Submodule 𝕜 E} (f : p →L[𝕜] F)
[FiniteDimensional 𝕜 (LinearMap.range f)] : ∃ g : E →L[𝕜] F, f = g.comp p.subtypeL :=
by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
set b := Module.finBasis 𝕜 (LinearMap.range f)
set e := b.equivFunL
set fi := fun i ↦ (LinearMap.toContinuousLinearMap (b.coord i)).comp (f.codRestrict _ <| LinearMap.mem_range_self _)
choose gi hgf _ using fun i ↦ exists_extension_norm_eq p (fi i)
use (LinearMap.range f).subtypeL.comp <| e.symm.toContinuousLinearMap.comp (.pi gi)
ext x
simp [fi, e, hgf]
