English
The vectorSpan of a finite affinely independent family has dimension one less than its cardinality.
Русский
ВекторSpan конечной аффинноправной семьи имеет размерность на единицу меньше её кардинала.
LaTeX
$$$\operatorname{finrank}_k\bigl(\operatorname{vectorSpan}_k(\operatorname{SetRange}(p))\bigr) + 1 = |\iota|$$$
Lean4
/-- `n + 1` points are affinely independent if and only if their
`vectorSpan` has dimension `n`. -/
theorem affineIndependent_iff_finrank_vectorSpan_eq [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 1) :
AffineIndependent k p ↔ finrank k (vectorSpan k (Set.range p)) = n := by
classical
have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
obtain ⟨i₁⟩ := hn
rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁, linearIndependent_iff_card_eq_finrank_span, eq_comm,
vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
rw [← Finset.card_univ] at hc
rw [Fintype.subtype_card]
simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]
