matrix_cramer — Mathlib

English

If A: X → M_n(R) and B: X → R^n are continuous, then the Cramer map x ↦ cramer(A(x), B(x)) is continuous.

Русский

Если A: X → M_n(R) и B: X → R^n непрерывны, то отображение x ↦ cramer(A(x), B(x)) непрерывно.

LaTeX

$$$\\operatorname{Continuous}(A) \\land \\operatorname{Continuous}(B) \\Rightarrow \\operatorname{Continuous}\\bigl(x \\mapsto \\operatorname{cramer}(A(x),B(x))\\bigr)$$$

Lean4

@[continuity, fun_prop]
theorem matrix_cramer [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R}
    {B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun x => cramer (A x) (B x) :=
  continuous_pi fun _ => (hA.matrix_updateCol _ hB).matrix_det

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