instT3Space — Mathlib

English

The matrix space CStarMatrix(m,n,A) is T3 (regular and T1) under the same assumptions as above, as it inherits this property from a product of T3 spaces.

Русский

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

LaTeX

$$$$\\text{T3Space}(\\mathrm{CStarMatrix}(m,n,A)).$$$$

Lean4

instance instT3Space : T3Space (CStarMatrix m n A) :=
  _root_.instT3Space

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