oangle_eq_zero_iff_wbtw — Mathlib

English

The oriented angle ∡ p1 p2 p3 is zero if and only if either p2 weakly lies between p1 and p3 or p2 weakly lies between p3 and p1.

Русский

Ориентированный угол ∡ p1 p2 p3 равен нулю тогда и только если p2 лежит между p1 и p3 в слабом смысле или между p3 и p1.

LaTeX

$$$\angle p_1 p_2 p_3 = 0 \iff Wbtw_\mathbb{R}(p_2,p_1,p_3) \lor Wbtw_\mathbb{R}(p_2,p_3,p_1)$$$

Lean4

/-- The oriented angle between three points is zero if and only if one of the first and third
points is weakly between the other two. -/
theorem oangle_eq_zero_iff_wbtw {p₁ p₂ p₃ : P} : ∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁ :=
  by
  by_cases hp₁p₂ : p₁ = p₂; · simp [hp₁p₂]
  by_cases hp₃p₂ : p₃ = p₂; · simp [hp₃p₂]
  rw [oangle_eq_zero_iff_angle_eq_zero hp₁p₂ hp₃p₂, angle_eq_zero_iff_ne_and_wbtw]
  simp [hp₁p₂, hp₃p₂]

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