orthonormal_subtype_iff_ite — Mathlib

English

Orthonormal 𝕜 v is equivalent to the condition ⟪v_i, v_j⟫ = δ_ij for all i,j, where δ_ij = 1 if i=j and 0 otherwise.

Русский

Ортонормированность 𝕜 v эквивалентна условию ⟪v_i, v_j⟫ = δ_ij для всех i,j, где δ_ij = 1 если i=j и 0 иначе.

LaTeX

$$$\operatorname{Orthonormal} 𝕜 v \iff \forall i j, \langle v_i, v_j \rangle = \delta_{ij} = \begin{cases}1 & i=j \\ 0 & i\neq j\end{cases}$$$

Lean4

/-- `if ... then ... else` characterization of a set of vectors being orthonormal.  (Inner product
equals Kronecker delta.) -/
theorem orthonormal_subtype_iff_ite [DecidableEq E] {s : Set E} :
    Orthonormal 𝕜 (Subtype.val : s → E) ↔ ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫ = if v = w then 1 else 0 :=
  by
  rw [orthonormal_iff_ite]
  simp

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