English
For an affinely independent family p, the cardinality of ι is at most finrank k (vectorSpan k (Set.range p)) + 1.
Русский
Для аффинно независимой семьи p кардинал множества индексов не превосходит размерности vectorSpan плюс единица.
LaTeX
$$$\operatorname{card}(\iota) \le \operatorname{finrank}_k\bigl(\operatorname{vectorSpan}_k(\operatorname{SetRange}(p))\bigr) + 1$$$
Lean4
theorem card_le_finrank_succ [Fintype ι] {p : ι → P} (hp : AffineIndependent k p) :
Fintype.card ι ≤ Module.finrank k (vectorSpan k (Set.range p)) + 1 :=
by
cases isEmpty_or_nonempty ι
· simp [Fintype.card_eq_zero]
rw [← tsub_le_iff_right]
exact
(affineIndependent_iff_le_finrank_vectorSpan _ _
(tsub_add_cancel_of_le <| Nat.one_le_iff_ne_zero.2 Fintype.card_ne_zero).symm).1
hp