coe_reindex — Mathlib

English

There is a natural linear isometry between the ambient spaces mapping one orthonormal basis to another; this is captured by b.equiv b' e.

Русский

Существует естественная линейно-изометричная карта между афинными пространствами, переводящая одну ортонормированную базу в другую; она задаётся как b.equiv b' e.

LaTeX

$$$$ \\mathrm{b}.\\mathrm{equiv}\\;\\mathrm{b'}\\;e : E \\to E' \\text{ is a linear isometry sending } b_i \\mapsto b'_{e(i)}. $$$$

Lean4

@[simp]
protected theorem coe_reindex (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') : ⇑(b.reindex e) = b ∘ e.symm :=
  funext (b.reindex_apply e)

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