coe_gramSchmidtBasis — Mathlib

English

If the input is linearly independent, then the normalized Gram–Schmidt vectors form an orthonormal system.

Русский

Если вход линейно независим, то нормированные векторы Gram–Schmidt образуют ортонормированную систему.

LaTeX

$$$$\text{If } f \text{ is LI, then } \mathrm{gramSchmidtNormed}_{\mathbb{K}} f \text{ is orthonormal}. $$$$

Lean4

theorem coe_gramSchmidtBasis (b : Basis ι 𝕜 E) : (gramSchmidtBasis b : ι → E) = gramSchmidt 𝕜 b :=
  Basis.coe_mk _ _

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