Theorems · Definition · functional analysis

WeakDual.seminormFamily

(𝕜 : Type u_1) →
  (E : Type u_3) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → SeminormFamily 𝕜 (WeakDual 𝕜 E) E

The family of seminorms on WeakDual 𝕜 E given by fun x f ↦ ‖f x‖, indexed by E. This is the seminorm family associated to the weak-\* topology via topDualPairing.

Defined in

Mathlib.Analysis.Normed.Module.WeakDual

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpace