locallyConvexSpace — Mathlib

English

If E and F are locally convex spaces over 𝕜, then the product space E × F, with the product topology, is locally convex over 𝕜.

Русский

Если E и F — локально выпуклые пространства над 𝕜, то произведение E × F с произведительной топологией локально выпукло над 𝕜.

LaTeX

$$$\text{LocallyConvexSpace } 𝕜 (E \times F)$$$

Lean4

instance locallyConvexSpace [TopologicalSpace E] [TopologicalSpace F] [LocallyConvexSpace 𝕜 E]
    [LocallyConvexSpace 𝕜 F] : LocallyConvexSpace 𝕜 (E × F) :=
  .inf (.induced (LinearMap.fst _ _ _)) (.induced (LinearMap.snd _ _ _))

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