gramSchmidtBasis — Mathlib

English

If the initial segment up to n is LI, then gramSchmidt 𝕜 f n ≠ 0 (coe variant).

Русский

Если начальный отрезок до n линейно независим, то gramSchmidt 𝕜 f n ≠ 0 (вариант коэ).

LaTeX

$$$$\text{If } (f \circ (\mathrm{↑} : \mathrm{Iic}\ n \to ι)) \text{ is LI, then } \mathrm{gramSchmidt}_{\mathbb{K}} f(n) \neq 0.$$$$

Lean4

/-- When given a basis, `gramSchmidt` produces a basis. -/
noncomputable def gramSchmidtBasis (b : Basis ι 𝕜 E) : Basis ι 𝕜 E :=
  Basis.mk (gramSchmidt_linearIndependent b.linearIndependent) ((span_gramSchmidt 𝕜 b).trans b.span_eq).ge

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