English
Let X be a topological space and R a topological ring. If A: X → M_n(R) is continuous, then x ↦ det(A(x)) is continuous.
Русский
Пусть X — топологическое пространство и R — топологическое кольцо. Если A: X → M_n(R) непрерывна, то x ↦ det(A(x)) непрерывна.
LaTeX
$$$\\operatorname{Continuous}(A) \\Rightarrow \\operatorname{Continuous}\\bigl(x \\mapsto \\det(A(x))\\bigr)$$$
Lean4
@[continuity, fun_prop]
theorem matrix_det [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R}
(hA : Continuous A) : Continuous fun x => (A x).det :=
by
simp_rw [Matrix.det_apply]
refine continuous_finset_sum _ fun l _ => Continuous.const_smul ?_ _
exact continuous_finset_prod _ fun l _ => hA.matrix_elem _ _
