English
For any three points p1, p2, p3, the angle ∠ p1 p2 p3 = 0 holds iff either p1 = p3 and p1 ≠ p2, or p2 lies between p1 and p3, or p2 lies between p3 and p1.
Русский
Для любых трёх точек p1, p2, p3 угол ∠ p1 p2 p3 = 0 эквивалентно либо p1 = p3 и p1 ≠ p2, либо p2 лежит между p1 и p3, либо p2 лежит между p3 и p1.
LaTeX
$$$$ \angle p_1 p_2 p_3 = 0 \iff (p_1 = p_3 \land p_1 \neq p_2) \lor \operatorname{Between}(p_2,p_1,p_3) \lor \operatorname{Between}(p_2,p_3,p_1). $$$$
Lean4
/-- The angle between three points is zero if and only if one of the first and third points is
strictly between the other two, or those two points are equal but not equal to the second. -/
theorem angle_eq_zero_iff_eq_and_ne_or_sbtw {p₁ p₂ p₃ : P} :
∠ p₁ p₂ p₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁ :=
by
rw [angle_eq_zero_iff_ne_and_wbtw]
by_cases hp₁p₂ : p₁ = p₂; · simp [hp₁p₂]
by_cases hp₁p₃ : p₁ = p₃; · simp [hp₁p₃]
by_cases hp₃p₂ : p₃ = p₂; · simp [hp₃p₂]
simp [hp₁p₂, hp₁p₃, Ne.symm hp₁p₃, Sbtw, hp₃p₂]
