matrix_conjTranspose — Mathlib

English

If A: X → M_{m×n}(R) is continuous, then its conjugate transpose A(x)ᴴ is continuous provided there is a continuous star on R.

Русский

Если A: X → M_{m×n}(R) непрерывна, то A(x)ᴴ непрерывно при существовании непрерывной операции звезды на R.

LaTeX

$$$\\operatorname{Continuous}(A) \\Rightarrow \\operatorname{Continuous}(x \\mapsto A(x)^{\\#})$$$

Lean4

@[continuity, fun_prop]
theorem matrix_conjTranspose [Star R] [ContinuousStar R] {A : X → Matrix m n R} (hA : Continuous A) :
    Continuous fun x => (A x)ᴴ :=
  hA.matrix_transpose.matrix_map continuous_star

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