English
If s is Collinear, p2 and p3 are in s with p2 ≠ p3, then Collinear k (insert p1 s) holds iff Collinear k ({p1, p2, p3}).
Русский
Если s коллинерен, p2 и p3 принадлежат s и p2 ≠ p3, тогда Collinear k (insert p1 s) эквивалентно Collinear k {p1, p2, p3}.
LaTeX
$$$Collinear_k(s) \to (p_2 \in s) (p_3 \in s) (p_2 \ne p_3) \Rightarrow Collinear_k(\operatorname{insert} p_1\; s) \Leftrightarrow Collinear_k(\{p_1,p_2,p_3\})$$$
Lean4
/-- Given a collinear set of points, and two distinct points `p₂` and `p₃` in it, a point `p₁` is
collinear with the set if and only if it is collinear with `p₂` and `p₃`. -/
theorem collinear_insert_iff_of_ne {s : Set P} (h : Collinear k s) {p₁ p₂ p₃ : P} (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s)
(hp₂p₃ : p₂ ≠ p₃) : Collinear k (insert p₁ s) ↔ Collinear k ({ p₁, p₂, p₃ } : Set P) :=
by
have hv : vectorSpan k (insert p₁ s) = vectorSpan k ({ p₁, p₂, p₃ } : Set P) :=
by
conv_rhs => rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, h.affineSpan_eq_of_ne hp₂ hp₃ hp₂p₃]
rw [Collinear, Collinear, hv]
