ne₁₂_of_not_collinear — Mathlib

English

If a triple is not collinear, then the first two points are distinct.

Русский

Если тройка не коллинеарна, то первые две точки различны.

LaTeX

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

Lean4

/-- If three points are not collinear, the first and second 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

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