matrix_submatrix — Mathlib

English

If A: X → n → R is continuous, then x ↦ replicateRow ι (A x) is continuous.

Русский

Если A: X → n → R непрерывна, то x ↦ replicateRow ι (A x) непрерывно по x.

LaTeX

$$$\\operatorname{Continuous}\\big(\\lambda x:\\,X,\\ replicateRow\\ ι\\ (A\\,x)\\big).$$$

Lean4

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

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