linearIndependent — Mathlib

English

An orthonormal family is linearly independent.

Русский

Ортонормированное семейство линейно независимо.

LaTeX

$$$\text{Orthonormal } 𝕜 v \Rightarrow \text{LinearIndependent } 𝕜 v$$$

Lean4

/-- An orthonormal set is linearly independent. -/
theorem linearIndependent {v : ι → E} (hv : Orthonormal 𝕜 v) : LinearIndependent 𝕜 v :=
  by
  rw [linearIndependent_iff]
  intro l hl
  ext i
  have key : ⟪v i, Finsupp.linearCombination 𝕜 v l⟫ = ⟪v i, 0⟫ := by rw [hl]
  simpa only [hv.inner_right_finsupp, inner_zero_right] using key

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