abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq

English

In an isosceles configuration, the base angle is acute: |∡ p1 p2 p3| < π/2 when dist p1 p2 = dist p1 p3.

Русский

В равнобедренной конфигурации основание угла остро: |∡ p1 p2 p3| < π/2 при равенстве dist(p1,p2) = dist(p1,p3).

LaTeX

$$$ dist(p_1,p_2) = dist(p_1,p_3) \Rightarrow |(\angle p_1 p_2 p_3).toReal| < \frac{\pi}{2}$$$

Lean4

/-- A base angle of an isosceles triangle is acute, oriented angle-at-point form. -/
theorem abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq {p₁ p₂ p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) :
    |(∡ p₂ p₃ p₁).toReal| < π / 2 :=
  oangle_eq_oangle_of_dist_eq h ▸ abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq h

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