Theorems · Theorem · geometry

Orientation.oangle_sign_smul_add_smul_left

∀ {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 : V) (r₁ r₂ : ℝ),
  (o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign

The sign of the angle between a linear combination of two vectors and the second vector is the sign of the factor by which the first vector is multiplied in that combination multiplied by the sign of the angle between the two vectors.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFact