sum_repr' — Mathlib

English

Let b be an orthonormal basis of a complex inner product space E. Then for any x ∈ E, the expansion can be written as the sum of inner products with the basis elements, using the first argument of the inner product: x = sum_i ⟪b_i, x⟫ b_i.

Русский

Пусть b — ортонормированный базис пространства E над 𝕜, тогда для любого x ∈ E разложение можно записать как x = ∑_i ⟪b_i, x⟫ b_i, используя первый аргумент скалярного произведения.

LaTeX

$$$\sum_i ⟪b_i, x⟫_𝕜 \; b_i = x$$$

Lean4

protected theorem sum_repr' (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i, ⟪b i, x⟫_𝕜 • b i = x :=
  by
  nth_rw 2 [← (b.sum_repr x)]
  simp_rw [b.repr_apply_apply x]

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