English
Let X be a topological space and R a topological ring. If A: X → M_n(R) is continuous, then the trace of A(x) depends continuously on x; i.e., x ↦ tr(A(x)) is a continuous function.
Русский
Пусть X — топологическое множество, R — топологическая кольцо. Если A: X → M_n(R) непрерывна, то tr(A(x)) непрерывна по x, т.е. x ↦ tr(A(x)) непрерывна.
LaTeX
$$$\\operatorname{Continuous}(A) \\Rightarrow \\operatorname{Continuous}\\bigl(x \\mapsto \\operatorname{trace}(A(x))\\bigr)$$$
Lean4
@[continuity, fun_prop]
theorem matrix_trace [Fintype n] [AddCommMonoid R] [ContinuousAdd R] {A : X → Matrix n n R} (hA : Continuous A) :
Continuous fun x => trace (A x) :=
continuous_finset_sum _ fun _ _ => hA.matrix_elem _ _
