English
For nonzero vectors x,y, the oriented angle equals π if and only if the unoriented angle equals π.
Русский
Для ненулевых векторов x,y ориентированный угол равен π тогда и только тогда, когда неориентированный угол равен π.
LaTeX
$$$ x \neq 0 \land y \neq 0 \Rightarrow o.oangle x y = \pi \iff InnerProductGeometry.angle x y = \pi $$$
Lean4
/-- The oriented angle between two vectors is `π` if and only if the unoriented angle is `π`. -/
theorem oangle_eq_pi_iff_angle_eq_pi {x y : V} : o.oangle x y = π ↔ InnerProductGeometry.angle x y = π :=
by
by_cases hx : x = 0
· simp [hx, Real.Angle.pi_ne_zero.symm, div_eq_mul_inv, Real.pi_ne_zero]
by_cases hy : y = 0
· simp [hy, Real.Angle.pi_ne_zero.symm, div_eq_mul_inv, Real.pi_ne_zero]
refine ⟨fun h => ?_, fun h => ?_⟩
· rw [o.angle_eq_abs_oangle_toReal hx hy, h]
simp [Real.pi_pos.le]
· have ha := o.oangle_eq_angle_or_eq_neg_angle hx hy
rw [h] at ha
simpa using ha
