sum_repr_symm — Mathlib

English

Let b be an orthonormal basis of E and v ∈ EuclideanSpace ι (coordinates). Then ∑ i v_i b_i equals the vector in E corresponding to v under the basis repr.symm.

Русский

Пусть b — ортонормированный базис пространства E и v ∈ EuclideanSpace ι; тогда ∑_i v_i b_i представляет вектор в E, соответствующий координатам v через отображение repr.symm.

LaTeX

$$$\sum_i v_i \; b_i = b.repr.symm(v)$$$

Lean4

protected theorem sum_repr_symm (b : OrthonormalBasis ι 𝕜 E) (v : EuclideanSpace 𝕜 ι) :
    ∑ i, v i • b i = b.repr.symm v := by simpa using (b.toBasis.equivFun_symm_apply v).symm

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