English
Let p : ι → P be affinely independent, with V finite-dimensional, and ι finite. Then the affine span of the image of p is the top subspace if and only if the cardinality of ι equals finrank k V + 1.
Русский
Пусть p : ι → P задаёт аффинно независимую семью точек; если V конечномерно над k, и ι конечно, то афинное охватывающее множество p равно верхнему подпространству тогда и только тогда, когдаcard(ι) = finrank_k(V) + 1.
LaTeX
$$$\operatorname{AffineIndependent}_k(p) \;\Rightarrow\; \bigl( \operatorname{affineSpan}_k(\{p(i) : i \in \iota\}) = \top \;\iff\; |\iota| = \operatorname{finrank} k V + 1 \bigr).$$$
Lean4
/-- The `affineSpan` of a finite affinely independent family is `⊤` iff the
family's cardinality is one more than that of the finite-dimensional space. -/
theorem affineSpan_eq_top_iff_card_eq_finrank_add_one [FiniteDimensional k V] [Fintype ι] {p : ι → P}
(hi : AffineIndependent k p) : affineSpan k (Set.range p) = ⊤ ↔ Fintype.card ι = finrank k V + 1 :=
by
constructor
· intro h_tot
let n := Fintype.card ι - 1
have hn : Fintype.card ι = n + 1 := (Nat.succ_pred_eq_of_pos (card_pos_of_affineSpan_eq_top k V P h_tot)).symm
rw [hn, ← finrank_top, ← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot, ← hi.finrank_vectorSpan hn]
· intro hc
rw [← finrank_top, ← direction_top k V P] at hc
exact hi.affineSpan_eq_of_le_of_card_eq_finrank_add_one le_top hc
