repr_apply_apply — Mathlib

English

The vector x in E can be reconstructed as the sum of its coefficients with respect to the Hilbert basis.

Русский

Вектор x в E восстанавливается как сумма его коэффициентов по Гильбертовой базе.

LaTeX

$$$ HasSum (\\lambda i, (b.repr x)_i · b_i) x $$$

Lean4

protected theorem repr_apply_apply (b : HilbertBasis ι 𝕜 E) (v : E) (i : ι) : b.repr v i = ⟪b i, v⟫ := by
  classical
  rw [← b.repr.inner_map_map (b i) v, b.repr_self, lp.inner_single_left]
  simp

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