Theorems · Theorem · functional analysis

StrongDual.norm_extendRCLike_le_seminorm

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : Module ℝ E]
  [inst_4 : IsScalarTower ℝ 𝕜 E] [inst_5 : TopologicalSpace E] [inst_6 : ContinuousConstSMul 𝕜 E] (fr : StrongDual ℝ E)
  {p : Seminorm 𝕜 E}, (∀ (x : E), |fr x| ≤ p x) → ∀ (x : E), ‖fr.extendRCLike x‖ ≤ p x

If a continuous real-linear functional is bounded by a 𝕜-seminorm, then its 𝕜-linear extension is bounded by the same seminorm.

Defined in

Mathlib.Analysis.Normed.Module.RCLike.Extend

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeAddCommGroupModuleModuleIsScalarTowerTopologicalSpaceContinuousConstSMul