Theorems · Theorem · geometry

Collinear.oangle_sign_of_sameRay_vsub

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ : P} (p₅ : P),
  p₁ ≠ p₂ →
    p₃ ≠ p₄ →
      Collinear ℝ {p₁, p₂, p₃, p₄} →
        SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃) →
          (EuclideanGeometry.oangle p₁ p₅ p₂).sign = (EuclideanGeometry.oangle p₃ p₅ p₄).sign

Given two pairs of distinct points on the same line, such that the vectors between those pairs of points are on the same ray (oriented in the same direction on that line), and a fifth point, the angles at the fifth point between each of those two pairs of points have the same sign.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented