Theorems · Theorem · functional analysis

StrongDual.exists_extension

∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] {𝕜 : Type u_3}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : Module 𝕜 E] [PolynormableSpace 𝕜 E]
  (S : Submodule 𝕜 E) (f : StrongDual 𝕜 ↥S), ∃ g, ∀ (x : ↥S), g ↑x = f x

Hahn-Banach theorem for continuous linear functionals on polynormable spaces over a field satisfying IsRCLikeNormedField.

Defined in

Mathlib.Analysis.LocallyConvex.HahnBanach

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupTopologicalSpaceNontriviallyNormedFieldIsRCLikeNormedFieldModulePolynormableSpace