orthonormal_single — Mathlib

English

The family of vectors i ↦ EuclideanSpace.single i (1) forms an orthonormal family.

Русский

Семейство векторов i ↦ EuclideanSpace.single i (1) образует ортонормированную совокупность.

LaTeX

$$Orthonormal 𝕜 (fun i => EuclideanSpace.single i (1 : 𝕜))$$

Lean4

/-- `EuclideanSpace.single` forms an orthonormal family. -/
theorem orthonormal_single : Orthonormal 𝕜 fun i : ι => EuclideanSpace.single i (1 : 𝕜) :=
  by
  simp_rw [orthonormal_iff_ite, EuclideanSpace.inner_single_left, map_one, one_mul, EuclideanSpace.single_apply]
  intros
  trivial

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