ne₂₃_of_not_collinear — Mathlib

English

Let p1, p2, p3 be points in P. If the three points {p1, p2, p3} are not collinear over k, then p2 ≠ p3.

Русский

Пусть p1, p2, p3 — точки в P. Если три точки {p1, p2, p3} не лежат на одной прямой относительно поля k, то p2 ≠ p3.

LaTeX

$$$\neg \operatorname{Collinear}_k\bigl(\{p_1,p_2,p_3\}\bigr) \Rightarrow p_2 \neq p_3$$$

Lean4

/-- If three points are not collinear, the second and third are different. -/
theorem ne₂₃_of_not_collinear {p₁ p₂ p₃ : P} (h : ¬Collinear k ({ p₁, p₂, p₃ } : Set P)) : p₂ ≠ p₃ :=
  by
  rintro rfl
  simp [collinear_pair] at h

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