English
The vector span after adding a point to an affine subspace with finite-dimensional direction remains finite-dimensional.
Русский
Векторное пространство, порождаемое добавлением точки к аффинному подпроstoранству с конечномерным направлением, остаётся конечномерным.
LaTeX
$$$\operatorname{FiniteDimensional}_k\bigl( \operatorname{vectorSpan}_k( \operatorname{insert} p ((s : Set P)) ) \bigr).$$$
Lean4
/-- The `vectorSpan` of adding a point to a finite-dimensional subspace is finite-dimensional. -/
instance finiteDimensional_vectorSpan_insert (s : AffineSubspace k P) [FiniteDimensional k s.direction] (p : P) :
FiniteDimensional k (vectorSpan k (insert p (s : Set P))) :=
by
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
rcases (s : Set P).eq_empty_or_nonempty with (hs | ⟨p₀, hp₀⟩)
· rw [coe_eq_bot_iff] at hs
rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan]
convert finiteDimensional_bot k V <;> simp
· rw [affineSpan_coe, direction_affineSpan_insert hp₀]
infer_instance
