oangle_eq_pi_sub_two_zsmul_oangle_center_right

English

Two equal congruence classes of base-point shift preserve the doubled base angle equality across two centers.

Русский

Две совпадающие конфигурации точек сохраняют удвоенный угловой показатель при изменении базиса.

LaTeX

$$(2)·oangle(y-x1, z-x1) = (2)·oangle(y-x2, z-x2)$$

Lean4

/-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented
angle-at-point form where the apex is given as the center of a circle. -/
theorem oangle_eq_pi_sub_two_zsmul_oangle_center_right {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
    (h : p₁ ≠ p₂) : ∡ p₁ s.center p₂ = π - (2 : ℤ) • ∡ p₂ p₁ s.center := by
  rw [oangle_eq_pi_sub_two_zsmul_oangle_center_left hp₁ hp₂ h,
    oangle_eq_oangle_of_dist_eq (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)]

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