gramSchmidtNormed_unit_length' — Mathlib

English

In a triangular arrangement, the inner product between the basis vector at j and the original vector at i vanishes when i < j.

Русский

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

LaTeX

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

Lean4

theorem gramSchmidtNormed_unit_length' {f : ι → E} {n : ι} (hn : gramSchmidtNormed 𝕜 f n ≠ 0) :
    ‖gramSchmidtNormed 𝕜 f n‖ = 1 := by
  rw [gramSchmidtNormed] at *
  rw [norm_smul_inv_norm]
  simpa using hn

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