Theorems · Theorem · functional analysis

ContinuousLinearMap.exist_extension_of_finiteDimensional_range

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : NormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜 E] [PolynormableSpace 𝕜 E] {F : Type u_3} [inst_6 : AddCommGroup F]
  [inst_7 : TopologicalSpace F] [IsTopologicalAddGroup F] [inst_9 : Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space F]
  {S : Submodule 𝕜 E} (f : ↥S →L[𝕜] F) [FiniteDimensional 𝕜 ↥(↑f).range], ∃ g, f = g ∘SL S.subtypeL

Corollary of the polynormable Hahn-Banach theorem: if f : S → F is a continuous linear map with finite-dimensional range, then f extends to a continuous linear map on the whole space.

Defined in

Mathlib.Analysis.LocallyConvex.HahnBanach

Cited by

1 results in Mathlib

Foundations

Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupNormedFieldIsRCLikeNormedFieldTopologicalSpaceModulePolynormableSpaceAddCommGroupTopologicalSpaceIsTopologicalAddGroupModuleContinuousSMulT2SpaceFiniteDimensional