instDiscreteTopologyMatrixOfFinite

English

If R has a discrete topology and m,n are finite, then the space of m×n matrices over R has the discrete topology.

Русский

Если у пространства R дискретная топология, и размеры матриц конечны, то пространство матриц размером m×n над R имеет дискретную топологию.

LaTeX

$$$\operatorname{DiscreteTopology}(M_{m,n}(R))$$$

Lean4

/-- The topology on finite matrices over a discrete space is discrete. -/
instance [TopologicalSpace R] [Finite m] [Finite n] [DiscreteTopology R] : DiscreteTopology (Matrix m n R) :=
  Pi.discreteTopology

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