matrix_transpose — Mathlib

English

If A: X → M_{m×n}(R) is continuous, then its transpose A(x)^T is continuous in x.

Русский

Если A: X → M_{m×n}(R) непрерывна, то A(x)^T по переменной x непрерывна.

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem matrix_transpose {A : X → Matrix m n R} (hA : Continuous A) : Continuous fun x => (A x)ᵀ :=
  continuous_matrix fun i j => hA.matrix_elem j i

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