equiv_apply_basis — Mathlib

English

The inverse equivalence between bases equals the other bases' equivalence with reversed indices.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem equiv_apply_basis (i : ι) : b.equiv b' e (b i) = b' (e i) := by
  classical
  simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self,
    LinearIsometryEquiv.piLpCongrLeft_apply]
  refine DFunLike.congr rfl ?_
  ext j
  simp [Equiv.symm_apply_eq]

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