Theorems · Definition · functional analysis

WeakDual.toStrongDual

{𝕜 : Type u_2} →
  {E : Type u_4} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → WeakDual 𝕜 E ≃ₗ[𝕜] StrongDual 𝕜 E

For vector spaces E, there is a canonical map WeakDual 𝕜 E → StrongDual 𝕜 E (the "identity" mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear equivalence StrongDual.toWeakDual in the other direction.

Defined in

Mathlib.Topology.Algebra.Module.Spaces.WeakDual

Cited by

20 results in Mathlib

Foundations

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

Assumes

CommSemiringTopologicalSpaceContinuousAddContinuousConstSMulAddCommMonoidModuleTopologicalSpace