oangle_eq_oangle_of_dist_eq — Mathlib

English

Oangle for swapped endpoints satisfies a rearranged sum identity: ∡ p₂ p p₃ + ∡ p₁ p p₂ = ∡ p₁ p p₃.

Русский

Угол при подстановке концов удовлетворяет перераспределенной тождественности: ∡ p₂ p p₃ + ∡ p₁ p p₂ = ∡ p₁ p p₃.

LaTeX

$$$ \forall p,p_1,p_2,p_3 : P,\ (\angle p_2 p p_3) + (\angle p_1 p p_2) = (\angle p_1 p p_3)$$$

Lean4

/-- Pons asinorum, oriented angle-at-point form. -/
theorem oangle_eq_oangle_of_dist_eq {p₁ p₂ p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) : ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁ :=
  by
  simp_rw [dist_eq_norm_vsub V] at h
  rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
    o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]

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