angle_pos_of_angle_eq_pi_div_two — Mathlib

English

In a nondegenerate right-angled triangle, the angle is positive: if ∠ p1 p2 p3 = π/2, then ∠ p2 p3 p1 > 0.

Русский

В невыраженной через degenerate форме прямоугольного треугольника угол положителен: если ∠ p1 p2 p3 = π/2, то ∠ p2 p3 p1 > 0.

LaTeX

$$$ \angle p_2 p_3 p_1 > 0 $$$

Lean4

/-- An angle in a non-degenerate right-angled triangle is positive. -/
theorem angle_pos_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) :
    0 < ∠ p₂ p₃ p₁ :=
  by
  rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
    neg_vsub_eq_vsub_rev] at h
  rw [← @vsub_ne_zero V, eq_comm, ← @vsub_eq_zero_iff_eq V, or_comm] at h0
  rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]
  exact angle_add_pos_of_inner_eq_zero h h0

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