equiv_trans — Mathlib

English

The canonical equivalence on a given orthonormal basis with the identity index bijection is the identity isometry on E.

Русский

Едениственный эквивалент по базису с индексной биекцияй равенство — это тождественная изометрия на E.

LaTeX

$$$hv.equiv hv (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E$$$

Lean4

@[simp]
theorem equiv_trans {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 v') (e : ι ≃ ι')
    {v'' : Basis ι'' 𝕜 E''} (hv'' : Orthonormal 𝕜 v'') (e' : ι' ≃ ι'') :
    (hv.equiv hv' e).trans (hv'.equiv hv'' e') = hv.equiv hv'' (e.trans e') :=
  v.ext_linearIsometryEquiv fun i => by
    simp only [LinearIsometryEquiv.trans_apply, Orthonormal.equiv_apply, e.coe_trans, Function.comp_apply]

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