locallyConvexSpace — Mathlib

English

If each X_i is a locally convex space over 𝕜, then the product space ∏_i X_i, with the product topology, is locally convex over 𝕜.

Русский

Если каждый X_i — локально выпукло над 𝕜, то произведение ∏_i X_i с произведительной топологией локально выпукло над 𝕜.

LaTeX

$$$\text{LocallyConvexSpace } 𝕜 (\prod_{i} X_i)$, given $\forall i, \text{LocallyConvexSpace } 𝕜 (X_i)$$$

Lean4

instance locallyConvexSpace {ι : Type*} {X : ι → Type*} [∀ i, AddCommMonoid (X i)] [∀ i, TopologicalSpace (X i)]
    [∀ i, Module 𝕜 (X i)] [∀ i, LocallyConvexSpace 𝕜 (X i)] : LocallyConvexSpace 𝕜 (∀ i, X i) :=
  .iInf fun i => .induced (LinearMap.proj i)

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