ne₁₃_of_not_collinear — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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