angle_eq_angle_of_dist_eq — Mathlib

English

If two sides of a triangle from a common vertex are equal, the base angles are equal.

Русский

Если две стороны равны, углы при вершинах у основания треугольника равны.

LaTeX

$$$\operatorname{dist}(p_1,p_2) = \operatorname{dist}(p_1,p_3) \Rightarrow \angle p_1 p_2 p_3 = \angle p_1 p_3 p_2$$$

Lean4

/-- **Isosceles Triangle Theorem**: Pons asinorum, angle-at-point form. -/
theorem angle_eq_angle_of_dist_eq {p₁ p₂ p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) : ∠ p₁ p₂ p₃ = ∠ p₁ p₃ p₂ :=
  by
  rw [dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃] at h
  unfold angle
  convert angle_sub_eq_angle_sub_rev_of_norm_eq h
  · exact (vsub_sub_vsub_cancel_left p₃ p₂ p₁).symm
  · exact (vsub_sub_vsub_cancel_left p₂ p₃ p₁).symm

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