Theorems · Theorem · geometry

Orientation.oangle_eq_of_angle_eq_of_sign_eq

∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {w x y z : V},
  InnerProductGeometry.angle w x = InnerProductGeometry.angle y z →
    (o.oangle w x).sign = (o.oangle y z).sign → o.oangle w x = o.oangle y z

If two unoriented angles are equal, and the signs of the corresponding oriented angles are equal, then the oriented angles are equal (even in degenerate cases).

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Cited by

3 results in Mathlib

Foundations

Depth 283 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceFact