English
If hi is affine independent and vectorSpan of s.image p is contained in sm with finite dimension, and |s| = finrank sm + 1, then vectorSpan equals sm.
Русский
Если hi аффинно независим и vectorSpan( s.image p ) ≤ sm с конечной размерностью и |s| = finrank sm + 1, тогда vectorSpan = sm.
LaTeX
$$$\text{AffineIndependent}_k(p) \Rightarrow (\text{vectorSpan}_k(\operatorname{image}(p,s)) \le sm) \Rightarrow \#s = \operatorname{finrank}_k(sm) + 1 \Rightarrow \operatorname{vectorSpan}_k(\operatorname{image}(p,s)) = sm$$$
Lean4
/-- If the `vectorSpan` of a finite affinely independent
family lies in a submodule with dimension one less than its
cardinality, it equals that submodule. -/
theorem vectorSpan_eq_of_le_of_card_eq_finrank_add_one [Fintype ι] {p : ι → P} (hi : AffineIndependent k p)
{sm : Submodule k V} [FiniteDimensional k sm] (hle : vectorSpan k (Set.range p) ≤ sm)
(hc : Fintype.card ι = finrank k sm + 1) : vectorSpan k (Set.range p) = sm :=
Submodule.eq_of_le_of_finrank_eq hle <| hi.finrank_vectorSpan hc
