coe_toBasis_repr_apply — Mathlib

English

The evaluation of the representation of toBasis on x at i equals the i-th coordinate of x in the basis representation.

Русский

Значение представления toBasis для x на i равно i-й координате x в представлении базиса.

LaTeX

$$b.toBasis.repr x i = b.repr x i$$

Lean4

@[simp]
protected theorem coe_toBasis_repr_apply (b : OrthonormalBasis ι 𝕜 E) (x : E) (i : ι) :
    b.toBasis.repr x i = b.repr x i :=
  by
  rw [← Basis.equivFun_apply, OrthonormalBasis.coe_toBasis_repr]
    -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644

  erw [LinearIsometryEquiv.coe_toLinearEquiv]

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