English
If the vector span of a set is finite-dimensional, then the vector span after inserting a point remains finite-dimensional as well.
Русский
Если векторное пространство порождается множеством с конечной размерностью, то добавление точки сохраняет конечномерность.
LaTeX
$$$\operatorname{FiniteDimensional}_k(\operatorname{vectorSpan}_k(\operatorname{insert} p \; s)).$$$
Lean4
/-- The `vectorSpan` of adding a point to a set with a finite-dimensional `vectorSpan` is
finite-dimensional. -/
instance finiteDimensional_vectorSpan_insert_set (s : Set P) [FiniteDimensional k (vectorSpan k s)] (p : P) :
FiniteDimensional k (vectorSpan k (insert p s)) :=
by
haveI : FiniteDimensional k (affineSpan k s).direction := (direction_affineSpan k s).symm ▸ inferInstance
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan]
exact finiteDimensional_vectorSpan_insert (affineSpan k s) p
