span_gramSchmidtNormed_range — Mathlib

English

In the dual triangular arrangement, the inner product with the i-th original vector vanishes for j > i.

Русский

В двойной треугольной схеме скалярное произведение с i-м исходным вектором равно нулю при j > i.

LaTeX

$$$$ \langle \mathrm{gramSchmidtOrthonormalBasis}(h,f)_j, f_i \rangle = 0 \quad \text{for } i

Lean4

theorem span_gramSchmidtNormed_range (f : ι → E) :
    span 𝕜 (range (gramSchmidtNormed 𝕜 f)) = span 𝕜 (range (gramSchmidt 𝕜 f)) := by
  simpa only [image_univ.symm] using span_gramSchmidtNormed f univ

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