matrix_adjugate — Mathlib

English

If A: X → M_n(R) is continuous, then x ↦ adjugate(A(x)) is continuous.

Русский

Если A: X → M_n(R) непрерывна, то x ↦ adjugate(A(x)) непрерывно по x.

LaTeX

$$$\\operatorname{Continuous}(A) \\Rightarrow \\operatorname{Continuous}\\bigl(x \\mapsto \\operatorname{adjugate}(A(x))\\bigr)$$$

Lean4

@[continuity, fun_prop]
theorem matrix_adjugate [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R}
    (hA : Continuous A) : Continuous fun x => (A x).adjugate :=
  continuous_matrix fun _j k => (hA.matrix_transpose.matrix_updateCol k continuous_const).matrix_det

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