English
If four points lie on a sphere, equalities of two doubled base angles hold for the corresponding opposite triples.
Русский
Если четыре точки лежат на сфере, то равенства удвоенных базовых углов верны для соответствующих пары тройки.
LaTeX
$$$2\\ oangle(p_1,p_2,p_4) = 2\\ oangle(p_1,p_3,p_4)$$$
Lean4
/-- Given two points on a circle, the radius of that circle may be expressed explicitly as half
the distance between those two points divided by the cosine of the angle between the chord and
the radius at one of those points. -/
theorem dist_div_cos_oangle_center_div_two_eq_radius {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
(h : p₁ ≠ p₂) : dist p₁ p₂ / Real.Angle.cos (∡ p₂ p₁ s.center) / 2 = s.radius :=
by
rw [div_right_comm, div_eq_mul_inv _ (2 : ℝ), mul_comm,
show (2 : ℝ)⁻¹ * dist p₁ p₂ = dist p₁ (midpoint ℝ p₁ p₂) by simp, ← mem_sphere.1 hp₁, ←
tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center hp₁ hp₂ h, ← oangle_midpoint_rev_left, oangle,
vadd_vsub_assoc, show p₂ -ᵥ p₁ = (2 : ℝ) • (midpoint ℝ p₁ p₂ -ᵥ p₁) by simp, map_smul, smul_smul,
div_mul_cancel₀ _ (two_ne_zero' ℝ), @dist_eq_norm_vsub' V, @dist_eq_norm_vsub' V, vadd_vsub_assoc, add_comm,
«o».oangle_add_right_smul_rotation_pi_div_two, Real.Angle.cos_coe, Real.cos_arctan]
· norm_cast
rw [one_div, div_inv_eq_mul, ← mul_self_inj (by positivity) (by positivity),
norm_add_sq_eq_norm_sq_add_norm_sq_real («o».inner_smul_rotation_pi_div_two_right _ _), ← mul_assoc, mul_comm,
mul_comm _ (√_), ← mul_assoc, ← mul_assoc, Real.mul_self_sqrt (by positivity), norm_smul,
LinearIsometryEquiv.norm_map]
conv_rhs => rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs, abs_mul_abs_self]
ring
· simpa using h.symm
