map_isometryOfOrthonormal — Mathlib

English

The inner product with basisFun i picks out the i-th coordinate.

Русский

Скалярное произведение с basisFun i извлекает i-ю координату.

LaTeX

$$$$ \\langle x, \\mathrm{basisFun}_{\\mathbb{R}}(i) \\rangle = x_i. $$$$

Lean4

@[simp]
theorem map_isometryOfOrthonormal (v : OrthonormalBasis (Fin 2) ℝ F) (f : F ≃ₗᵢ[ℝ] F') :
    Complex.isometryOfOrthonormal (v.map f) = (Complex.isometryOfOrthonormal v).trans f :=
  by
  simp only [isometryOfOrthonormal, OrthonormalBasis.map, LinearIsometryEquiv.symm_trans, LinearIsometryEquiv.symm_symm]
    -- Porting note: `LinearIsometryEquiv.trans_assoc` doesn't trigger in the `simp` above

  rw [LinearIsometryEquiv.trans_assoc]

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