secondInter_collinear — Mathlib

English

The points p, p', and s.secondInter p (p' - p) are collinear.

Русский

Точки p, p' и s.secondInter p (p' - p) коллинеарны.

LaTeX

$$Collinear(\\mathbb{R}, \\{p,p',s.secondInter(p,p'-p)\\})$$

Lean4

/-- If the vector passed to `secondInter` is given by a subtraction involving the point in
`secondInter`, the three points are collinear. -/
theorem secondInter_collinear (s : Sphere P) (p p' : P) : Collinear ℝ ({p, p', s.secondInter p (p' -ᵥ p)} : Set P) :=
  by
  rw [Set.pair_comm, Set.insert_comm]
  exact (collinear_insert_iff_of_mem_affineSpan (s.secondInter_vsub_mem_affineSpan _ _)).2 (collinear_pair ℝ _ _)

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