finiteDimensional_vectorSpan_range

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 _)

Похожие утверждения