finiteDimensional_direction_affineSpan

English

The vector span of a collinear set is finite-dimensional (as a subspace).

Русский

Векторное пространство коллинеарного множества конечномерно.

LaTeX

$$$\operatorname{finiteDimensional_vectorSpan}(s) :\; \text{if } \operatorname{Collinear}_k(s) \text{ then } \operatorname{FiniteDimensional}_k(\operatorname{vectorSpan}_k s).$$$

Lean4

/-- The direction of the affine span of collinear points is finite-dimensional. -/
theorem finiteDimensional_direction_affineSpan {s : Set P} (h : Collinear k s) :
    FiniteDimensional k (affineSpan k s).direction :=
  (direction_affineSpan k s).symm ▸ h.finiteDimensional_vectorSpan

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