gramSchmidtNormed_unit_length_coe

English

If the initial segment up to n is LI, then the norm of gramSchmidtNormed f n equals 1.

Русский

Если начальный отрезок до n линейно независим, то нормa вектора gramSchmidtNormed f n равна 1.

LaTeX

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

Lean4

theorem gramSchmidtNormed_unit_length_coe {f : ι → E} (n : ι) (h₀ : LinearIndependent 𝕜 (f ∘ ((↑) : Set.Iic n → ι))) :
    ‖gramSchmidtNormed 𝕜 f n‖ = 1 := by
  simp only [gramSchmidt_ne_zero_coe n h₀, gramSchmidtNormed, norm_smul_inv_norm, Ne, not_false_iff]

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