English
The lemma bounds the finrank of the vector span after inserting a point into an affine subspace.
Русский
Лемма ограничивает размерность векторного Span после вставки точки в аффинное подпространство.
LaTeX
$$finrank_k( vectorSpan_k( insert p ((s:Set P)) )) ≤ finrank_k( vectorSpan_k s ) + 1$$
Lean4
/-- Adding a point to a collinear set produces a coplanar set. -/
theorem coplanar_insert {s : Set P} (h : Collinear k s) (p : P) : Coplanar k (insert p s) :=
by
have : FiniteDimensional k { x // x ∈ vectorSpan k s } := h.finiteDimensional_vectorSpan
rw [coplanar_iff_finrank_le_two]
exact (finrank_vectorSpan_insert_le_set k s p).trans (add_le_add_right h.finrank_le_one _)