coe_ofRepr — Mathlib

English

The EuclideanSpace 𝕜-valued basis e that assigns to each index i the vector EuclideanSpace.single i (1) forms an orthonormal set (or basis) in the sense of inner product spaces.

Русский

Система векторов i ↦ EuclideanSpace.single i (1) образует ортонормированный базис Евклидова пространства.

LaTeX

$$Orthonormal 𝕜 (fun i : ι => EuclideanSpace.single i (1 : 𝕜))$$

Lean4

@[simp]
theorem coe_ofRepr [DecidableEq ι] (e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) :
    ⇑(OrthonormalBasis.ofRepr e) = fun i => e.symm (EuclideanSpace.single i (1 : 𝕜)) :=
  by
  dsimp only [DFunLike.coe]
  funext
  congr!

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