affineIndependent_iff_not_finrank_vectorSpan_le

English

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

Русский

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

LaTeX

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

Lean4

/-- `n + 2` points are affinely independent if and only if their
`vectorSpan` does not have dimension at most `n`. -/
theorem affineIndependent_iff_not_finrank_vectorSpan_le [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 2) :
    AffineIndependent k p ↔ ¬finrank k (vectorSpan k (Set.range p)) ≤ n := by
  rw [affineIndependent_iff_le_finrank_vectorSpan k p hc, ← Nat.lt_iff_add_one_le, lt_iff_not_ge]

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