locallyConvexSpace — Mathlib

English

For any B, the real vector space WeakBilin(B) carries a locally convex space structure, induced by the seminorm family coming from B (via B.weakBilin_withSeminorms).

Русский

Для любого B слабое билинеарное пространство WeakBilin(B) оснащено структуройLocallyConvexSpace over ℝ, задаваемой семинормами из B (через B.weakBilin_withSeminorms).

LaTeX

$$$\\operatorname{LocallyConvexSpace}_{\\mathbb{R}}(\\mathrm{WeakBilin}(B))$$$

Lean4

instance locallyConvexSpace {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} : LocallyConvexSpace ℝ (WeakBilin B) :=
  B.weakBilin_withSeminorms.toLocallyConvexSpace

Похожие утверждения