oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq

English

If p1,p2,p3 form an isosceles configuration with p2 as apex, then ∡ p3 p1 p2 = π − 2∡ p1 p2 p3.

Русский

При равнобедренной конфигурации вершина p2, угол вершины равен π − 2∡ p1 p2 p3.

LaTeX

$$$ \forall p_1,p_2,p_3 : P,\ (\text{dist } p_1 p_2 = \text{dist } p_1 p_3) \Rightarrow \angle p_3 p_1 p_2 = \pi - 2 \angle p_1 p_2 p_3$$$

Lean4

/-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented
angle-at-point form. -/
theorem oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq {p₁ p₂ p₃ : P} (hn : p₂ ≠ p₃) (h : dist p₁ p₂ = dist p₁ p₃) :
    ∡ p₃ p₁ p₂ = π - (2 : ℤ) • ∡ p₁ p₂ p₃ :=
  by
  simp_rw [dist_eq_norm_vsub V] at h
  rw [oangle, oangle]
  convert o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq _ h using 1
  · rw [← neg_vsub_eq_vsub_rev p₁ p₃, ← neg_vsub_eq_vsub_rev p₁ p₂, o.oangle_neg_neg]
  · rw [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]; simp
  · simpa using hn

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