finiteDimensional_direction_affineSpan_insert

English

The direction of the affine span of adding a point to a finite-dimensional subspace remains finite-dimensional.

Русский

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

LaTeX

$$$\operatorname{FiniteDimensional}_k\bigl( (\operatorname{affineSpan}_k( \operatorname{insert} p (s) ) ).\text{direction} \bigr).$$$

Lean4

/-- The direction of the affine span of adding a point to a finite-dimensional subspace is
finite-dimensional. -/
instance finiteDimensional_direction_affineSpan_insert (s : AffineSubspace k P) [FiniteDimensional k s.direction]
    (p : P) : FiniteDimensional k (affineSpan k (insert p (s : Set P))).direction :=
  (direction_affineSpan k (insert p (s : Set P))).symm ▸ finiteDimensional_vectorSpan_insert s p

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