instT2SpaceMatrix — Mathlib

English

If R is a Hausdorff space, then the matrix space M_{m,n}(R) is a Hausdorff space with the product topology.

Русский

Если R является пространством Хаусдорфа, то пространство матриц M_{m,n}(R) тоже является пространством Хаусдорфа с произведением топологий.

LaTeX

$$$\text{T2Space}(M_{m,n}(R))$$$

Lean4

instance [TopologicalSpace R] [T2Space R] : T2Space (Matrix m n R) :=
  Pi.t2Space

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