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 lie on a common sphere.
Русский
Если четыре точки p1,p2,p3,p4 удовлетворяют условию, что 2 угла между p1 и p4 с вершиной p2 равны 2 углам между p1 и p4 с вершиной p3, и точки p1,p2,p4 не лежат на одной прямой, тогда все четыре точки лежат на одной сфере.
LaTeX
$$$2\angle(p_1,p_2,p_4) = 2\angle(p_1,p_3,p_4) \;\Rightarrow\; \text{Cospherical}\{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 π. -/
theorem cospherical_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)) :
Cospherical ({ p₁, p₂, p₃, p₄ } : Set P) :=
by
have hn' : ¬Collinear ℝ ({ p₁, p₃, p₄ } : Set P) := by rwa [← collinear_iff_of_two_zsmul_oangle_eq h]
let t₁ : Affine.Triangle ℝ P := ⟨![p₁, p₂, p₄], affineIndependent_iff_not_collinear_set.2 hn⟩
let t₂ : Affine.Triangle ℝ P := ⟨![p₁, p₃, p₄], affineIndependent_iff_not_collinear_set.2 hn'⟩
rw [cospherical_iff_exists_sphere]
refine ⟨t₂.circumsphere, ?_⟩
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]
refine ⟨t₂.mem_circumsphere 0, ?_, t₂.mem_circumsphere 1, t₂.mem_circumsphere 2⟩
rw [Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq (by decide : (0 : Fin 3) ≠ 1)
(by decide : (0 : Fin 3) ≠ 2) (by decide) (show t₂.points 0 = t₁.points 0 from rfl) rfl h.symm]
exact t₁.mem_circumsphere 1
