gramSchmidtNormed_unit_length — Mathlib

English

If the input is linearly independent, then gramSchmidtNormed f has unit length for all indices.

Русский

Если вход линейно независим, то gramSchmidtNormed f имеет длину 1 для всех индексов.

LaTeX

$$$$\|\mathrm{gramSchmidtNormed}_{\mathbb{K}} f\| = 1.$$$$

Lean4

theorem gramSchmidtNormed_unit_length {f : ι → E} (n : ι) (h₀ : LinearIndependent 𝕜 f) :
    ‖gramSchmidtNormed 𝕜 f n‖ = 1 :=
  gramSchmidtNormed_unit_length_coe _ (LinearIndependent.comp h₀ _ Subtype.coe_injective)

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