English
For any three points p1, p2, p3, the angle ∠ p1 p2 p3 equals 0 precisely when either p1 ≠ p2 and p2 is between p1 and p3, or p3 ≠ p2 and p2 is between p3 and p1.
Русский
Для любых трёх точек p1, p2, p3 угол ∠ p1 p2 p3 равен нулю тогда и только тогда, когда либо p1 ≠ p2 и p2 лежит между p1 и p3, либо p3 ≠ p2 и p2 лежит между p3 и p1.
LaTeX
$$$$ \forall p_1,p_2,p_3,\; \angle p_1 p_2 p_3 = 0 \iff (p_1 \neq p_2 \land \operatorname{Between}(p_2,p_1,p_3)) \lor (p_3 \neq p_2 \land \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
weakly between the other two, and not equal to the second. -/
theorem angle_eq_zero_iff_ne_and_wbtw {p₁ p₂ p₃ : P} :
∠ p₁ p₂ p₃ = 0 ↔ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ :=
by
constructor
· rw [angle, angle_eq_zero_iff]
rintro ⟨hp₁p₂, r, hr0, hp₃p₂⟩
rcases le_or_gt 1 r with (hr1 | hr1)
· refine Or.inl ⟨vsub_ne_zero.1 hp₁p₂, r⁻¹, ⟨(inv_pos.2 hr0).le, inv_le_one_of_one_le₀ hr1⟩, ?_⟩
rw [AffineMap.lineMap_apply, hp₃p₂, smul_smul, inv_mul_cancel₀ hr0.ne.symm, one_smul, vsub_vadd]
· refine Or.inr ⟨?_, r, ⟨hr0.le, hr1.le⟩, ?_⟩
· rw [← @vsub_ne_zero V, hp₃p₂, smul_ne_zero_iff]
exact ⟨hr0.ne.symm, hp₁p₂⟩
· rw [AffineMap.lineMap_apply, ← hp₃p₂, vsub_vadd]
· rintro (⟨hp₁p₂, h⟩ | ⟨hp₃p₂, h⟩)
· exact h.angle₂₁₃_eq_zero_of_ne hp₁p₂
· exact h.angle₃₁₂_eq_zero_of_ne hp₃p₂
