21.3. Locally convex spaces🔗

Mathlib contains an extensive theory of locally convex spaces. The basic way to instantiate a LCTVS is as follows:

variable (E 𝕜 : Type*) [NormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [TopologicalSpace E]
  [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [NormedSpace ℝ 𝕜] [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
  [LocallyConvexSpace ℝ E]

For coefficients more general than ℝ or ℂ there is also PolynormableSpace.

To say that E is a TVS whose topology is generated by a family of seminorms one writes:

variable {ι : Type*} (E 𝕜 : Type*) [NormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [TopologicalSpace E]
  [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p)

and Mathlib knows that in this case the space is locally convex:

example
    [NormedSpace ℝ 𝕜] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] :
    LocallyConvexSpace ℝ E := hp.toLocallyConvexSpace