Theorems · Definition · functional analysis

LinearMap.toSeminormFamily

{𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : AddCommGroup F] → [inst_4 : Module 𝕜 F] → (E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → SeminormFamily 𝕜 E F

Construct a family of seminorms from a bilinear form.

Defined in

Mathlib.Analysis.LocallyConvex.WeakDual

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedFieldAddCommGroupModuleAddCommGroupModule