collinear_insert_insert_of_mem_affineSpan_pair

English

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

Русский

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

LaTeX

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

Lean4

/-- If two points lie in the affine span of two points, those four points are collinear. -/
theorem collinear_insert_insert_of_mem_affineSpan_pair {p₁ p₂ p₃ p₄ : P} (h₁ : p₁ ∈ line[k, p₃, p₄])
    (h₂ : p₂ ∈ line[k, p₃, p₄]) : Collinear k ({ p₁, p₂, p₃, p₄ } : Set P) :=
  by
  rw [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 _ _ _

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