matrix_reindex — Mathlib

English

If A: X → M_{l×n}(R) is continuous, then for any e1 : m → l and e2 : p → n, the submatrix A(x).submatrix e1 e2 is continuous in x.

Русский

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

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem matrix_reindex {A : X → Matrix l n R} (hA : Continuous A) (e₁ : l ≃ m) (e₂ : n ≃ p) :
    Continuous fun x => reindex e₁ e₂ (A x) :=
  hA.matrix_submatrix _ _

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