finiteDimensional_vectorSpan_singleton

English

The vector span of a singleton {p} is finite-dimensional.

Русский

Векторное пространство, порождаемое множеством-одиночкой {p}, имеет конечную размерность.

LaTeX

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

Lean4

/-- The vector span of a singleton is finite-dimensional. -/
instance finiteDimensional_vectorSpan_singleton (p : P) : FiniteDimensional k (vectorSpan k { p }) :=
  finiteDimensional_vectorSpan_of_finite _ (Set.finite_singleton p)

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