finiteDimensional_vectorSpan_of_finite

English

If s is a finite subset of points, then the vector span of s is finite-dimensional over k.

Русский

Если s — конечное множество точек, то вектоpное пространство, порождаемое s, имеет конечную размерность над k.

LaTeX

$$$\operatorname{FiniteDimensional}_k(\operatorname{vectorSpan}_k s)$$$

Lean4

/-- The `vectorSpan` of a finite set is finite-dimensional. -/
theorem finiteDimensional_vectorSpan_of_finite {s : Set P} (h : Set.Finite s) : FiniteDimensional k (vectorSpan k s) :=
  .span_of_finite k <| h.vsub h

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