repr_reindex — Mathlib

English

The inverse of the equivalence between two bases corresponds to swapping the roles of the bases.

Русский

Обратный к эквивалентности переход между базами соответствует взаимной симметрии баз.

LaTeX

$$$$ (b.equiv b' e)^{-1} = (b'.equiv b e^{-1}). $$$$

Lean4

@[simp]
protected theorem repr_reindex (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') (x : E) (i' : ι') :
    (b.reindex e).repr x i' = b.repr x (e.symm i') := by
  classical rw [OrthonormalBasis.repr_apply_apply, b.repr_apply_apply, OrthonormalBasis.coe_reindex, comp_apply]

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