collinear_insert_of_mem_affineSpan_pair

English

If p1 lies in the affine span of {p2, p3}, then {p1, p2, p3} are collinear.

Русский

Если p1 лежит на прямой через p2 и p3, то p1, p2, p3 коллинеарны.

LaTeX

$$p_1 \in affineSpan_k{p_2,p_3} \Rightarrow Collinear_k\{p_1,p_2,p_3\}$$

Lean4

/-- If a point lies in the affine span of two points, those three points are collinear. -/
theorem collinear_insert_of_mem_affineSpan_pair {p₁ p₂ p₃ : P} (h : p₁ ∈ line[k, p₂, p₃]) :
    Collinear k ({ p₁, p₂, p₃ } : Set P) :=
  by
  rw [collinear_insert_iff_of_mem_affineSpan h]
  exact collinear_pair _ _ _

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