finiteDimensional_direction_affineSpan_of_finite

English

The direction (the associated linear subspace) of the affine span of any finite subset is finite-dimensional.

Русский

Направление аффинного охвата конечного множества точек является конечномерным подпростуком.

LaTeX

$$$\operatorname{FiniteDimensional}_k\bigl(\operatorname{direction}(\operatorname{affineSpan}_k s)\bigr)$$$

Lean4

/-- The direction of the affine span of a finite set is
finite-dimensional. -/
theorem finiteDimensional_direction_affineSpan_of_finite {s : Set P} (h : Set.Finite s) :
    FiniteDimensional k (affineSpan k s).direction :=
  (direction_affineSpan k s).symm ▸ finiteDimensional_vectorSpan_of_finite k h

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