collinear_insert_iff_of_mem_affineSpan

English

If p lies in the affine span of a set s, then adding p does not change whether the set is collinear: Collinear(k, insert p s) is equivalent to Collinear(k, s).

Русский

Если точка p лежит в аффинальной оболочке множества s, добавление p не меняет коллинерность: Collinear(k, insert p s) ⇔ Collinear(k, s).

LaTeX

$$p ∈ affineSpan(k, s) → Collinear_k(insert p s) ↔ Collinear_k s$$

Lean4

/-- Adding a point in the affine span of a set does not change whether that set is collinear. -/
theorem collinear_insert_iff_of_mem_affineSpan {s : Set P} {p : P} (h : p ∈ affineSpan k s) :
    Collinear k (insert p s) ↔ Collinear k s := by rw [Collinear, Collinear, vectorSpan_insert_eq_vectorSpan h]

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