Theorems · Theorem · functional analysis

Module.Dual.exists_extension_of_le_seminorm_real

∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (S : Subspace ℝ E) (f : Module.Dual ℝ ↥S)
  {p : Seminorm ℝ E}, (∀ (x : ↥S), f x ≤ p ↑x) → ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), |g x| ≤ p x

Defined in

Mathlib.Analysis.LocallyConvex.HahnBanach

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupModule