singleton — Mathlib

English

Two formulations of the equality between a basis-derived orthonormal basis and the original basis.

Русский

Существуют две формулировки равенства между ортонормированным базисом и исходным базисом.

LaTeX

$$$(v.toOrthonormalBasis hv).toBasis = v$$$

Lean4

/-- `OrthonormalBasis.singleton ι 𝕜` is the orthonormal basis sending the unique element of `ι` to
`1 : 𝕜`. -/
protected noncomputable def singleton : OrthonormalBasis ι 𝕜 𝕜 :=
  (Basis.singleton ι 𝕜).toOrthonormalBasis (by simp [orthonormal_iff_ite, Unique.eq_default])

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