English
If s is a Collinear set of points, and p1, p2, p3 ∈ s with p1 ≠ p2, then p3 lies on the line through p1 and p2, i.e., p3 ∈ line(k, p1, p2).
Русский
Если s — коллинеарный набор точек, и p1, p2, p3 ∈ s с p1 ≠ p2, то p3 лежит на прямой через p1 и p2, то есть p3 ∈ line(k, p1, p2).
LaTeX
$$Collinear_k(s) → (p1 ∈ s) → (p2 ∈ s) → (p3 ∈ s) → p1 ≠ p2 → p3 ∈ line_k(p1,p2)$$
Lean4
/-- A point in a collinear set of points lies in the affine span of any two distinct points of
that set. -/
theorem mem_affineSpan_of_mem_of_ne {s : Set P} (h : Collinear k s) {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
(hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) : p₃ ∈ line[k, p₁, p₂] :=
by
rw [collinear_iff_of_mem hp₁] at h
rcases h with ⟨v, h⟩
rcases h p₂ hp₂ with ⟨r₂, rfl⟩
rcases h p₃ hp₃ with ⟨r₃, rfl⟩
rw [vadd_left_mem_affineSpan_pair]
refine ⟨r₃ / r₂, ?_⟩
have h₂ : r₂ ≠ 0 := by
rintro rfl
simp at hp₁p₂
simp [smul_smul, h₂]
