toEuclideanCLM_toLp — Mathlib

English

For a matrix A and a vector x, applying the Euclidean CLM to the lp-vector given by x equals the lp-vector of A acting on x.

Русский

Для матрицы A и вектора x применение \n toEuclideanCLM к lp-вектору, полученному из x, даёт lp-вектор, получаемый при действия A на x.

LaTeX

$$$toEuclideanCLM(A)(toLp(x)) = toLp(A \\cdot x)$$$

Lean4

@[simp]
theorem toEuclideanCLM_toLp (A : Matrix n n 𝕜) (x : n → 𝕜) :
    toEuclideanCLM (n := n) (𝕜 := 𝕜) A (toLp _ x) = toLp _ (A *ᵥ x) :=
  rfl

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