concyclic_of_two_zsmul_oangle_eq_of_not_collinear

English

If four points p1,p2,p3,p4 satisfy 2 times the angle at p2 between p1 and p4 equals 2 times the angle at p3 between p1 and p4, and p1,p2,p4 are not collinear, then the four points are concyclic.

Русский

Если четыре точки p1,p2,p3,p4 удовлетворяют 2 угловым равенствам и p1,p2,p4 не коллинеарны, то точки лежат на одной окружности.

LaTeX

$$$2\angle(p_1,p_2,p_4) = 2\angle(p_1,p_3,p_4) \Rightarrow \text{Concyclic}\{p_1,p_2,p_3,p_4\}$, при условии неколлинеарности. $$

Lean4

/-- Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral
add to π", for oriented angles mod π, with a "concyclic" conclusion. -/
theorem concyclic_of_two_zsmul_oangle_eq_of_not_collinear {p₁ p₂ p₃ p₄ : P}
    (h : (2 : ℤ) • ∡ p₁ p₂ p₄ = (2 : ℤ) • ∡ p₁ p₃ p₄) (hn : ¬Collinear ℝ ({ p₁, p₂, p₄ } : Set P)) :
    Concyclic ({ p₁, p₂, p₃, p₄ } : Set P) :=
  ⟨cospherical_of_two_zsmul_oangle_eq_of_not_collinear h hn, coplanar_of_fact_finrank_eq_two _⟩

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