Oriented angles between three vectors of a common nonzero sign

For vectors x, y, z of an oriented real inner product space of dimension two such that y and z lie on the same open side of the line through x — their oriented angles from x have the same nonzero sign — Mathlib's Orientation.oangle_sub_left gives oangle y z = oangle x z - oangle x y, and this identity holds for the real representatives in (-π, π] as well (Orientation.oangle_toReal_sub_of_sign_eq, from Real.Angle.toReal_sub_of_sign_eq). Consequently the real angles from x add (Orientation.oangle_toReal_add_of_sign_eq), and oangle y z has positive sign exactly when the real angle of y from x is smaller than that of z (Orientation.oangle_sign_eq_one_iff_toReal_lt_of_sign_eq).

theorem Orientation.oangle_toReal_sub_of_sign_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V} (hs : (o.oangle x y).sign = (o.oangle x z).sign) (h0 : (o.oangle x y).sign ≠ 0) : (o.oangle y z).toReal = (o.oangle x z).toReal - (o.oangle x y).toReal

For two vectors y, z on the same open side of the line through x (their oriented angles from x have the same nonzero sign), the real oriented angle from y to z is the difference of their real angles from x.

theorem Orientation.oangle_toReal_add_of_sign_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V} (hs : (o.oangle x y).sign = (o.oangle x z).sign) (h0 : (o.oangle x y).sign ≠ 0) : (o.oangle x z).toReal = (o.oangle x y).toReal + (o.oangle y z).toReal

For two vectors y, z on the same open side of the line through x, the real angles from x add: the angle to z is the angle to y plus the angle from y to z.

theorem Orientation.oangle_sign_eq_one_iff_toReal_lt_of_sign_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V} (hs : (o.oangle x y).sign = (o.oangle x z).sign) (h0 : (o.oangle x y).sign ≠ 0) : (o.oangle y z).sign = 1 ↔ (o.oangle x y).toReal < (o.oangle x z).toReal

For two vectors y, z on the same open side of the line through x, the oriented angle from y to z is positive exactly when the angle of y from x is smaller than that of z.