Theorems · Theorem · functional analysis

orthonormal_iff_ite

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : DecidableEq ι] {v : ι → E},
  Orthonormal 𝕜 v ↔ ∀ (i j : ι), inner 𝕜 (v i) (v j) = if i = j then 1 else 0

if ... then ... else characterization of an indexed set of vectors being orthonormal. (Inner product equals Kronecker delta.)

Defined in

Mathlib.Analysis.InnerProductSpace.Orthonormal

Cited by

15 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeSeminormedAddCommGroupInnerProductSpaceDecidableEq