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