reindex — Mathlib

English

Definition of span-based orthonormal basis, producing an orthonormal basis for the span of a finite subset of an orthonormal family.

Русский

Определение ортонормированной базы, построенной для линейного замыкания конечного подмножества ортонормированной семейства.

LaTeX

$$$$ \\mathrm{span}\\_k(h,s) : \\text{OrthonormalBasis } s \\text{ for } \\operatorname{span}_k( s\\text{ image of } v'). $$$$

Lean4

/-- `b.reindex (e : ι ≃ ι')` is an `OrthonormalBasis` indexed by `ι'` -/
def reindex (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') : OrthonormalBasis ι' 𝕜 E :=
  OrthonormalBasis.ofRepr (b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e))

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