English
If two-angle equality holds between four points and not-collinear condition is met, then the four points are cospherical.
Русский
Если выполнено равенство двух углов между четырьмя точками и неколлинеарность, то точки лежат на одной сфере.
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 π, with a "cospherical or collinear" conclusion. -/
theorem cospherical_or_collinear_of_two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ : P}
(h : (2 : ℤ) • ∡ p₁ p₂ p₄ = (2 : ℤ) • ∡ p₁ p₃ p₄) :
Cospherical ({ p₁, p₂, p₃, p₄ } : Set P) ∨ Collinear ℝ ({ p₁, p₂, p₃, p₄ } : Set P) :=
by
by_cases hc : Collinear ℝ ({ p₁, p₂, p₄ } : Set P)
· by_cases he : p₁ = p₄
· rw [he, Set.insert_eq_self.2 (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))]
by_cases hl : Collinear ℝ ({ p₂, p₃, p₄ } : Set P); · exact Or.inr hl
rw [or_iff_left hl]
let t : Affine.Triangle ℝ P := ⟨![p₂, p₃, p₄], affineIndependent_iff_not_collinear_set.2 hl⟩
rw [cospherical_iff_exists_sphere]
refine ⟨t.circumsphere, ?_⟩
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]
exact ⟨t.mem_circumsphere 0, t.mem_circumsphere 1, t.mem_circumsphere 2⟩
have hc' : Collinear ℝ ({ p₁, p₃, p₄ } : Set P) := by rwa [← collinear_iff_of_two_zsmul_oangle_eq h]
refine Or.inr ?_
rw [Set.insert_comm p₁ p₂] at hc
rwa [Set.insert_comm p₁ p₂,
hc'.collinear_insert_iff_of_ne (Set.mem_insert _ _)
(Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))) he]
· exact Or.inl (cospherical_of_two_zsmul_oangle_eq_of_not_collinear h hc)
