matrix_diagonal — Mathlib

English

If A: X → n → R is continuous, then the diagonal vector diag(A(x)) is continuous in x.

Русский

Если A: X → n → R непрерывна, то диагональный вектор diag(A(x)) непрерывен по x.

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem matrix_diagonal [Zero R] [DecidableEq n] {A : X → n → R} (hA : Continuous A) :
    Continuous fun x => diagonal (A x) :=
  continuous_matrix fun i _ => ((continuous_apply i).comp hA).if_const _ continuous_zero

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