toBasis — Mathlib

English

The underlying basis of an orthonormal basis is the Basis ι 𝕜 E obtained from the representation equivalence.

Русский

Базис, лежащий в основе ортонормированного базиса, является базисом Basis ι 𝕜 E через эквивалентность представления.

LaTeX

$$b.toBasis = Basis.ofEquivFun b.repr.toLinearEquiv$$

Lean4

/-- The `Basis ι 𝕜 E` underlying the `OrthonormalBasis` -/
protected def toBasis (b : OrthonormalBasis ι 𝕜 E) : Basis ι 𝕜 E :=
  Basis.ofEquivFun b.repr.toLinearEquiv

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