orthonormal — Mathlib

English

The basis b is an orthonormal family, i.e., the basis vectors are pairwise orthogonal and of unit norm.

Русский

Базис b образует ортонормированную совокупность: векторы базиса ортогональны попарно и имеют норму 1.

LaTeX

$$Orthonormal 𝕜 b$$

Lean4

@[simp]
protected theorem orthonormal (b : OrthonormalBasis ι 𝕜 E) : Orthonormal 𝕜 b := by
  classical
  rw [orthonormal_iff_ite]
  intro i j
  rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j, EuclideanSpace.inner_single_left,
    EuclideanSpace.single_apply, map_one, one_mul]

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