English
If the signs of two oriented angles are equal and the unoriented angles are equal, then the oriented angles are equal.
Русский
Если знаки двух ориентированных углов равны и неориентированные углы равны, то сами ориентированные углы равны.
LaTeX
$$$ (\angle w x) = (\angle y z) \land (o.oangle w x).sign = (o.oangle y z).sign \Rightarrow o.oangle w x = o.oangle y z $$$
Lean4
/-- If the signs of two oriented angles between nonzero vectors are equal, the oriented angles are
equal if and only if the unoriented angles are equal. -/
theorem angle_eq_iff_oangle_eq_of_sign_eq {w x y z : V} (hw : w ≠ 0) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0)
(hs : (o.oangle w x).sign = (o.oangle y z).sign) :
InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z :=
by
refine ⟨fun h => o.oangle_eq_of_angle_eq_of_sign_eq h hs, fun h => ?_⟩
rw [o.angle_eq_abs_oangle_toReal hw hx, o.angle_eq_abs_oangle_toReal hy hz, h]
