instContinuousNegMatrix — Mathlib

English

Negation of matrices is continuous: the map A ↦ −A from M_{m×n}(R) to itself is continuous.

Русский

Отрицание матриц непрерывно: карта A ↦ −A из M_{m×n}(R) в себя непрерывна.

LaTeX

$$$\\operatorname{Continuous}\\big(\\lambda A : \\mathrm{M}_{m\\times n}(R) \\to \\mathrm{M}_{m\\times n}(R),\\ A \\mapsto -A\\big).$$$

Lean4

instance [Neg R] [ContinuousNeg R] : ContinuousNeg (Matrix m n R) :=
  Pi.continuousNeg

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