gramSchmidtOrthonormalBasis_apply

English

For nonzero Gram-Schmidt vectors, the orthonormal basis vector equals the corresponding Gram-Schmidt vector.

Русский

Для ненулевых векторов Gram-Schmidt в составе ортонормированного базиса совпадает с соответствующим вектором Gram-Schmidt.

LaTeX

$$$$ \text{If } \mathrm{gramSchmidtNormed}_{\mathbb{K}} f(i) \neq 0, \quad \mathrm{gramSchmidtOrthonormalBasis}(h,f)_i = \mathrm{gramSchmidtNormed}_{\mathbb{K}} f(i). $$$$

Lean4

theorem gramSchmidtOrthonormalBasis_apply {f : ι → E} {i : ι} (hi : gramSchmidtNormed 𝕜 f i ≠ 0) :
    gramSchmidtOrthonormalBasis h f i = gramSchmidtNormed 𝕜 f i :=
  ((gramSchmidtNormed_orthonormal' f).exists_orthonormalBasis_extension_of_card_eq (v := gramSchmidtNormed 𝕜 f)
        h).choose_spec
    i hi

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