coplanar_insert — Mathlib

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 _)

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