finiteDimensional_direction_affineSpan_range

English

For a finite subset s ⊆ P, the direction of its affine span is finite-dimensional.

Русский

Для конечного подмножества s ⊆ P направление аффинного охвата конечномерно.

LaTeX

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

Lean4

/-- The direction of the affine span of a family indexed by a
`Fintype` is finite-dimensional. -/
instance finiteDimensional_direction_affineSpan_range [Finite ι] (p : ι → P) :
    FiniteDimensional k (affineSpan k (Set.range p)).direction :=
  finiteDimensional_direction_affineSpan_of_finite k (Set.finite_range _)

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