Theorems · Theorem · functional analysis

NormedSpace.inclusionInDoubleDualWeak_apply

∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (X : Type u_2) [inst_1 : SeminormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (x : WeakSpace 𝕜 X),
  (NormedSpace.inclusionInDoubleDualWeak 𝕜 X) x =
    StrongDual.toWeakDual ((NormedSpace.inclusionInDoubleDual 𝕜 X) ((toWeakSpace 𝕜 X).symm x))

Defined in

Mathlib.Analysis.Normed.Module.DoubleDual

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpace