stdOrthonormalBasis — Mathlib

English

There is an explicit orthonormal basis for the Euclidean mixed space, built as the product of the real and complex bases, reindexed appropriately.

Русский

Существует явная ортонормированная база евклидова смешанного пространства, представленная как произведение баз для вещественной и комплексной частей с соответствующей переиндексацией.

LaTeX

$$stdOrthonormalBasis : OrthonormalBasis (index K) \mathbb{R} (\mathrm{mixedEmbedding.euclidean.mixedSpace}(K)).$$

Lean4

/-- An orthonormal basis of the Euclidean mixed space. -/
def stdOrthonormalBasis : OrthonormalBasis (index K) ℝ (euclidean.mixedSpace K) :=
  OrthonormalBasis.prod (EuclideanSpace.basisFun _ ℝ)
    ((Pi.orthonormalBasis fun _ ↦ Complex.orthonormalBasisOneI).reindex (Equiv.sigmaEquivProd _ _))

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