Theorems · Theorem · functional analysis

Submodule.ClosedComplemented.of_finiteDimensional

∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [IsRCLikeNormedField 𝕜] {F : Type u_3} [inst_2 : AddCommGroup F]
  [inst_3 : TopologicalSpace F] [IsTopologicalAddGroup F] [inst_5 : Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space F]
  [PolynormableSpace 𝕜 F] (S : Submodule 𝕜 F) [FiniteDimensional 𝕜 ↥S], S.ClosedComplemented

A finite-dimensional submodule of a polynormable space over a field satisfying IsRCLikeNormedField is Submodule.ClosedComplemented.

Defined in

Mathlib.Analysis.LocallyConvex.HahnBanach

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedFieldIsRCLikeNormedFieldAddCommGroupTopologicalSpaceIsTopologicalAddGroupModuleContinuousSMulT2SpacePolynormableSpaceFiniteDimensional