repr_symm_single — Mathlib

English

For any i, the representation of the symmetric image under repr evaluated at the i-th unit vector in EuclideanSpace corresponds to the i-th standard basis element.

Русский

Для любого i представление отображения через repr применяемое к единичному вектору с индексом i даёт i-й базисный вектор.

LaTeX

$$b.repr.symm (EuclideanSpace.single i (1 : 𝕜)) = b i$$

Lean4

@[simp]
protected theorem repr_symm_single [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
    b.repr.symm (EuclideanSpace.single i (1 : 𝕜)) = b i :=
  by
  dsimp only [DFunLike.coe]
  congr!

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