basisFun_inner — Mathlib

English

The canonical embedding (coercion) of OrthonormalBasis.mkOfOrthogonalEqBot hon hsp is exactly the original basis v.

Русский

Встроение (коэрцировка) OrthonormalBasis.mkOfOrthogonalEqBot hon hsp совпадает с исходной базой v.

LaTeX

$$$$ \\mathrm{OrthonormalBasis.coe\\_mk\\_of\\_OrthogonalEqBot}(hon,hsp) = v. $$$$

Lean4

@[simp]
theorem basisFun_inner (x : EuclideanSpace 𝕜 ι) (i : ι) : ⟪basisFun ι 𝕜 i, x⟫ = x i := by
  simp [← OrthonormalBasis.repr_apply_apply]

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