collinear_pair — Mathlib

English

Two points are collinear: the set {p1, p2} is collinear.

Русский

Две точки коллинеарны: множество {p1, p2} коллинеарно.

LaTeX

$$$\operatorname{Collinear}_k\bigl(\{p_1,p_2\}\bigr)$$$

Lean4

/-- Two points are collinear. -/
theorem collinear_pair (p₁ p₂ : P) : Collinear k ({ p₁, p₂ } : Set P) :=
  by
  rw [collinear_iff_exists_forall_eq_smul_vadd]
  use p₁, p₂ -ᵥ p₁
  intro p hp
  rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp
  rcases hp with hp | hp
  · use 0
    simp [hp]
  · use 1
    simp [hp]

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