gramSchmidt_ne_zero — Mathlib

English

If the input family f is linearly independent, then for every index n the vector gramSchmidt 𝕜 f n is nonzero.

Русский

Если входная система векторов линейно независима, то для каждого индекса n вектор gramSchmidt 𝕜 f n ненулевой.

LaTeX

$$$$\text{If } f \text{ is LI, then } \mathrm{gramSchmidt}_{\mathbb{K}} f(n) \neq 0 \quad \text{for all } n.$$$$

Lean4

/-- If the input vectors of `gramSchmidt` are linearly independent,
then the output vectors are non-zero. -/
theorem gramSchmidt_ne_zero {f : ι → E} (n : ι) (h₀ : LinearIndependent 𝕜 f) : gramSchmidt 𝕜 f n ≠ 0 :=
  gramSchmidt_ne_zero_coe _ (LinearIndependent.comp h₀ _ Subtype.coe_injective)

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