toLocallyConvexSpace — Mathlib

English

If E is a normed space over a field 𝕜, then E viewed as a real vector space is a locally convex space.

Русский

Если E — нормированное пространство над полем 𝕜, то, рассматривая его как вещественное векторное пространство, оно локально выпукло.

LaTeX

$$$ LocallyConvexSpace \\mathbb{R} E $$$

Lean4

/-- See `NormedSpace.toLocallyConvexSpace'` for a slightly stronger version which is not an
instance. -/
instance toLocallyConvexSpace [NormedSpace ℝ E] : LocallyConvexSpace ℝ E :=
  NormedSpace.toLocallyConvexSpace' ℝ

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