finiteDimensional_direction_affineSpan_image_of_finite

English

The direction of the affine span of a finite subset of indices image is finite-dimensional.

Русский

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

LaTeX

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

Lean4

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

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