Theorems · Theorem · geometry

Orientation.oangle_sub_right

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

Given three nonzero vectors, the angle between the first and the third minus the angle between the second and the third equals the angle between the first and the second.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFact