orthogonalFamily — Mathlib

English

In a finite index setting, the inner product with a finite sum reduces to the sum of inner products with individual terms.

Русский

В конечной индексации скалярное произведение с суммой равно сумме скалярных произведений по членам.

LaTeX

$$$\langle V_i v, \sum_j V_j (l_j) \rangle = \langle v, l_i \rangle$$$

Lean4

theorem orthogonalFamily {v : ι → E} (hv : Orthonormal 𝕜 v) :
    OrthogonalFamily 𝕜 (fun _i : ι => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E (hv.1 i) := fun i j hij a b => by
  simp [inner_smul_left, inner_smul_right, hv.2 hij]

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