English
The equivalence isomorphism between two orthonormal bases corresponds to the underlying linear equivalence as a linear map.
Русский
Эквивалентность между двумя ортонормированными базисами соответствует их линейной эквивалентности как линейному отображению.
LaTeX
$$$hv.equiv hv' e$ toLinearEquiv = v.equiv v' e$$
Lean4
/-- A linear isometric equivalence that sends an orthonormal basis to a given orthonormal basis. -/
def equiv {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 v') (e : ι ≃ ι') :
E ≃ₗᵢ[𝕜] E' :=
(v.equiv v' e).isometryOfOrthonormal hv
(by
have h : v.equiv v' e ∘ v = v' ∘ e := by
ext i
simp
rw [h]
classical exact hv'.comp _ e.injective)