ofLp_toEuclideanCLM — Mathlib

English

The preimage under toEuclideanCLM of the lp-vector is the matrix-vector product with A.

Русский

Образ предобраза под toEuclideanCLM от lp-вектора равен произведению матрицы A на вектор.

LaTeX

$$$ofLp(toEuclideanCLM(A, x)) = A *ᵥ ofLp(x)$$$

Lean4

@[simp]
theorem ofLp_toEuclideanCLM (A : Matrix n n 𝕜) (x : EuclideanSpace 𝕜 n) :
    ofLp (toEuclideanCLM (n := n) (𝕜 := 𝕜) A x) = A *ᵥ ofLp x :=
  rfl

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