continuous_matrix_diag — Mathlib

English

The function diag: M_{n×n}(R) → R^n that maps a matrix to its diagonal entries is continuous.

Русский

Функция diag: M_{n×n}(R) → R^n, извлекающая диагональные элементы матрицы, непрерывна.

LaTeX

$$$\\operatorname{Continuous}\\big(\\operatorname{diag} : \\mathrm{M}_{n\\times n}(R) \\to \\mathbb{R}^n\\big).$$$

Lean4

theorem continuous_matrix_diag : Continuous (Matrix.diag : Matrix n n R → n → R) :=
  show Continuous fun x : Matrix n n R => Matrix.diag x from continuous_id.matrix_diag

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