reindex_toBasis — Mathlib

English

The reindexed orthonormal basis has as its toBasis exactly the reindexed basis.

Русский

Переиндексированный ортонормированный базис имеет равную себе toBasis, полученную путем переиндексации.

LaTeX

$$$$ (\\mathrm{OrthonormalBasis}.reindex\\; e).\\mathrm{toBasis} = \\mathrm{OrthonormalBasis}.toBasis\\; \\mathrm{reindex}(e) $$$$

Lean4

@[simp]
theorem reindex_toBasis (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') : (b.reindex e).toBasis = b.toBasis.reindex e :=
  Basis.eq_ofRepr_eq_repr fun _ ↦ congr_fun rfl

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