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