English
If α acts continuously on R and the scalar action α × R → R is continuous, then the natural action of α on the space of m×n matrices with entries in R is continuous; i.e., the map (a, A) ↦ a · A from α × M_{m×n}(R) to M_{m×n}(R) is continuous.
Русский
Если на R действует непрерывно множество α, и соответствующее действие α × R → R непрерывно, то естественное действие α на пространстве матриц m×n над R непрерывно; то есть карта (a, A) ↦ a · A из α × M_{m×n}(R) в M_{m×n}(R) непрерывна.
LaTeX
$$$\\operatorname{Continuous}\\big(\\lambda (a,A) : \\alpha \\times \\mathrm{M}_{m\\times n}(R) \\to \\mathrm{M}_{m\\times n}(R),\\ (a,A) \\mapsto a\\cdot A\\big).$$$
Lean4
instance [TopologicalSpace α] [SMul α R] [ContinuousSMul α R] : ContinuousSMul α (Matrix m n R) :=
inferInstanceAs (ContinuousSMul α (m → n → R))
