collinear_insert_insert_insert_of_mem_affineSpan_pair

English

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

Русский

Если p1, p2, p3 лежат в аффинальной оболочке {p4, p5}, то все пять точек лежат на одной прямой.

LaTeX

$$p_1,p_2,p_3 ∈ affineSpan_k{p_4,p_5} ⇒ Collinear_k{p_1,p_2,p_3,p_4,p_5}$$

Lean4

/-- If three points lie in the affine span of two points, those five points are collinear. -/
theorem collinear_insert_insert_insert_of_mem_affineSpan_pair {p₁ p₂ p₃ p₄ p₅ : P} (h₁ : p₁ ∈ line[k, p₄, p₅])
    (h₂ : p₂ ∈ line[k, p₄, p₅]) (h₃ : p₃ ∈ line[k, p₄, p₅]) : Collinear k ({ p₁, p₂, p₃, p₄, p₅ } : Set P) :=
  by
  rw [collinear_insert_iff_of_mem_affineSpan
      ((AffineSubspace.le_def' _ _).1 (affineSpan_mono k ((Set.subset_insert _ _).trans (Set.subset_insert _ _))) _ h₁),
    collinear_insert_iff_of_mem_affineSpan
      ((AffineSubspace.le_def' _ _).1 (affineSpan_mono k (Set.subset_insert _ _)) _ h₂),
    collinear_insert_iff_of_mem_affineSpan h₃]
  exact collinear_pair _ _ _

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