English
Let E be a finite-dimensional inner product space over the field 𝕜 (where 𝕜 is a complex-like field). If b is an orthonormal basis {b_i} of E, then every vector x ∈ E can be reconstructed by its projections onto the basis: x = sum_i ⟨x, b_i⟩ b_i.
Русский
Пусть E — конечномерное пространство с вложенным скалярным произведением над полем 𝕜 (похожим на комплексное). Если b = {b_i} — ортонормированный базис E, то любой вектор x ∈ E может быть восстановлен по формулам проекции: x = ∑_i ⟨x, b_i⟩ b_i.
LaTeX
$$$\\sum_i ⟪x, b_i\\rangle b_i = x$$$
Lean4
protected theorem sum_repr (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i, b.repr x i • b i = x :=
by
simp_rw [← b.coe_toBasis_repr_apply, ← b.coe_toBasis]
exact b.toBasis.sum_repr x
