equiv — Mathlib

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)

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