instTopologicalSpace — Mathlib

English

The space of matrices CStarMatrix(m,n,A) is equipped with the product topology, i.e., the topology is the product of the topologies on A over all entries.

Русский

Пространство матриц CStarMatrix(m,n,A) снабжено произведением топологий по всем элементам, то есть топология задается как произведение топологий над A.

LaTeX

$$$$\\text{Top}(\\,\\mathrm{CStarMatrix}(m,n,A)\\,) = \\prod_{i\\in m}\\prod_{j\\in n} \\mathcal{T}_A,$$$$

Lean4

instance instTopologicalSpace : TopologicalSpace (CStarMatrix m n A) :=
  Pi.topologicalSpace

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