English
The oriented angle equals 0 or π exactly when either x = 0 or y is a scalar multiple of x.
Русский
Угол равен нулю или π тогда, когда либо x = 0, либо y = r·x для некоторого r ∈ ℝ.
LaTeX
$$$o.oangle x y = 0 \lor o.oangle x y = \pi \iff x = 0 \lor \exists r\in\mathbb{R},\ y = r\,x$$$
Lean4
/-- The oriented angle between two vectors is `π` if and only they are nonzero and the first is
on the same ray as the negation of the second. -/
theorem oangle_eq_pi_iff_sameRay_neg {x y : V} : o.oangle x y = π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) :=
by
rw [← o.oangle_eq_zero_iff_sameRay]
constructor
· intro h
by_cases hx : x = 0; · simp [hx, Real.Angle.pi_ne_zero.symm] at h
by_cases hy : y = 0; · simp [hy, Real.Angle.pi_ne_zero.symm] at h
refine ⟨hx, hy, ?_⟩
rw [o.oangle_neg_right hx hy, h, Real.Angle.coe_pi_add_coe_pi]
· rintro ⟨hx, hy, h⟩
rwa [o.oangle_neg_right hx hy, ← Real.Angle.sub_coe_pi_eq_add_coe_pi, sub_eq_zero] at h
