English
Let p be a finite family of points in an affine space over k. Then the vector span of the range of p is a finite-dimensional k-vector space.
Русский
Пусть p задаёт конечную семью точек в аффинном пространстве над полем k. Тогда векторное span множества p(ι) образует конечномерное пространство над k.
LaTeX
$$$\operatorname{FiniteDimensional}_k\bigl(\operatorname{vectorSpan}_k(\operatorname{SetRange}(p))\bigr)$$$
Lean4
/-- The `vectorSpan` of a family indexed by a `Fintype` is
finite-dimensional. -/
instance finiteDimensional_vectorSpan_range [Finite ι] (p : ι → P) : FiniteDimensional k (vectorSpan k (Set.range p)) :=
finiteDimensional_vectorSpan_of_finite k (Set.finite_range _)