isometryOfOrthonormal_symm_apply — Mathlib

English

The basisFun basis in Euclidean space equals PiLp.basisFun

Русский

База basisFun Евклидова пространства совпадает с PiLp.basisFun

LaTeX

$$$$ \\mathrm{basisFun}_{\\mathbb{R}} = \\mathrm{PiLp}.basisFun. $$$$

Lean4

theorem isometryOfOrthonormal_symm_apply (v : OrthonormalBasis (Fin 2) ℝ F) (f : F) :
    (Complex.isometryOfOrthonormal v).symm f = (v.toBasis.coord 0 f : ℂ) + (v.toBasis.coord 1 f : ℂ) * I := by
  simp [Complex.isometryOfOrthonormal]

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