finrank_vectorSpan_le_iff_not_affineIndependent

English

For a finite ι with card ι = n+2, finrank of vectorSpan k (Set.range p) ≤ n iff p is not affine independent.

Русский

Для конечного множества индексов ι с card ι = n+2, finrank vectorSpan ≤ n тогда и только тогда, когда p не аффинно независим.

LaTeX

$$$\operatorname{finrank}_k(\operatorname{vectorSpan}_k(\operatorname{SetRange}(p))) \le n \iff \lnot \text{AffineIndependent}_k(p)$$$

Lean4

/-- `n + 2` points have a `vectorSpan` with dimension at most `n` if
and only if they are not affinely independent. -/
theorem finrank_vectorSpan_le_iff_not_affineIndependent [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 2) :
    finrank k (vectorSpan k (Set.range p)) ≤ n ↔ ¬AffineIndependent k p :=
  (not_iff_comm.1 (affineIndependent_iff_not_finrank_vectorSpan_le k p hc).symm).symm

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