dist_eq_of_angle_eq_angle_of_angle_ne_pi

English

If angle equality holds for two angles and the third is not π, then the two side lengths are equal (norms).

Русский

Если равенство двух углов выполняется и третий не равен π, значит две стороны равны.

LaTeX

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

Lean4

/-- Converse of pons asinorum, angle-at-point form. -/
theorem dist_eq_of_angle_eq_angle_of_angle_ne_pi {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = ∠ p₁ p₃ p₂) (hpi : ∠ p₂ p₁ p₃ ≠ π) :
    dist p₁ p₂ = dist p₁ p₃ := by
  unfold angle at h hpi
  rw [dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃]
  rw [← angle_neg_neg, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev] at hpi
  rw [← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁] at h
  exact norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi h hpi

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