Theorems · Theorem · geometry

Orientation.angle_eq_iff_oangle_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},
  w ≠ 0 →
    x ≠ 0 →
      y ≠ 0 →
        z ≠ 0 →
          (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)

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.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFact