matrix_diag — Mathlib

English

If A: X → M_{l×n}(R) is continuous, then reindexing by equivalences e1,e2 yields a continuous matrix: x ↦ reindex e1 e2 (A x).

Русский

Если A: X → M_{l×n}(R) непрерывна, то при перестановке индексов по эквиваленциям e1,e2 получаем непрерывную матрицу: x ↦ reindex e1 e2 (A x).

LaTeX

$$$\\operatorname{Continuous}\\big(\\lambda x:\\,X,\\ \\operatorname{reindex}(e_1,e_2)(A\\,x)\\big).$$$

Lean4

@[continuity, fun_prop]
theorem matrix_diag {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun x => Matrix.diag (A x) :=
  continuous_pi fun _ =>
    hA.matrix_elem _
      _
        -- note this doesn't elaborate well from the above

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