instTopologicalSpaceMatrix — Mathlib

English

The topology on the space of m×n matrices over a topological space R is the product topology (the same as the product of mn copies of R).

Русский

Топология пространства матриц размером m×n над топологическим пространством R есть произведение, то есть топология RM×n аналогична произведению mn копий R.

LaTeX

$$$\operatorname{Top}(M_{m,n}(R)) = \operatorname{Pi.topologicalSpace}$$$

Lean4

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

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