matrix_elem — Mathlib

English

If A: X → M_{m×n}(R) is continuous, then each coordinate A(x)_{ij} is a continuous function of x.

Русский

Если A: X → M_{m×n}(R) непрерывна, то каждый элемент A(x)_{ij} — непрерывная функция от x.

LaTeX

$$$\\operatorname{Continuous}(A) \\Rightarrow \\forall i,j,\\ \\operatorname{Continuous}(x \\mapsto A(x)_{ij}).$$$

Lean4

theorem matrix_elem {A : X → Matrix m n R} (hA : Continuous A) (i : m) (j : n) : Continuous fun x => A x i j :=
  (continuous_apply_apply i j).comp hA

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