posDef_gram_iff_linearIndependent

English

In a normed space, PosDef (gram 𝕜 v) if and only if LinearIndependent 𝕜 v.

Русский

В нормированном пространстве PosDef (gram 𝕜 v) эквивалентно LinearIndependent 𝕜 v.

LaTeX

$$$ \text{PosDef }( \text{gram } 𝕜 v ) \iff \text{LinearIndependent } 𝕜 v $$$

Lean4

/-- In a normed space, linear independence of `v` is equivalent to positive definiteness of
`gram 𝕜 v`. -/
theorem posDef_gram_iff_linearIndependent {v : n → E} : PosDef (gram 𝕜 v) ↔ LinearIndependent 𝕜 v :=
  ⟨linearIndependent_of_posDef_gram, posDef_gram_of_linearIndependent⟩

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