Theorems · Inductive type · functional analysis

PolynormableSpace

(𝕜 : Type u_2) →
  (E : Type u_6) →
    [inst : NormedField 𝕜] → [inst_1 : AddCommGroup E] → [Module 𝕜 E] → [topology : TopologicalSpace E] → Prop

A topological vector space E is polynormable over 𝕜 if its topology is induced by some family of 𝕜-seminorms. Equivalently, its topology is induced by all its continuous seminorm. If 𝕜 is RCLike, this is equivalent to LocallyConvexSpace 𝕜 E.

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

15 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

NormedFieldAddCommGroupModuleTopologicalSpace