eq_ite — Mathlib

English

For an OrthogonalFamily, the inner product of the images equals the appropriate value with a case split on i = j.

Русский

Для ортогональной семьи скалярное произведение между образами равно соответствующему значению при разбиении на случай i = j и иначе.

LaTeX

$$$\langle V_i v, V_j w\rangle = \begin{cases} \langle V_i v, V_j w\rangle, & i=j \\ 0, & i\neq j \end{cases}$$$

Lean4

theorem eq_ite [DecidableEq ι] {i j : ι} (v : G i) (w : G j) : ⟪V i v, V j w⟫ = ite (i = j) ⟪V i v, V j w⟫ 0 :=
  by
  split_ifs with h
  · rfl
  · exact hV h v w

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