affineIndependent_iff_le_finrank_vectorSpan

English

For a finite index set ι with card ι = n+1, p: ι → P is affine independent iff finrank of vectorSpan k (Set.range p) is n.

Русский

Для конечного множества индексов ι с card ι = n+1; p: ι → P аффинно независим тогда и только тогда, когда finrank vectorSpan k (Set.range p) равно n.

LaTeX

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

Lean4

/-- `n + 1` points are affinely independent if and only if their
`vectorSpan` has dimension at least `n`. -/
theorem affineIndependent_iff_le_finrank_vectorSpan [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 1) :
    AffineIndependent k p ↔ n ≤ finrank k (vectorSpan k (Set.range p)) :=
  by
  rw [affineIndependent_iff_finrank_vectorSpan_eq k p hc]
  constructor
  · rintro rfl
    rfl
  · exact fun hle => le_antisymm (finrank_vectorSpan_range_le k p hc) hle

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