equiv_apply_euclideanSpace — Mathlib

English

The representation of basisFun equals the coordinate map; evaluating a vector x against basisFun yields the i-th coordinate.

Русский

Представление basisFun даёт координату i для вектора x.

LaTeX

$$$$ (\\mathrm{basisFun}_{\\mathbb{R}}).\\mathrm{repr}(x)(i) = x_i. $$$$

Lean4

theorem equiv_apply_euclideanSpace (x : EuclideanSpace 𝕜 ι) :
    (EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι) x = ∑ i, x i • b i := by
  simp_rw [equiv_apply, EuclideanSpace.basisFun_repr, Equiv.refl_apply]

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