Theorems · Theorem · geometry

Sbtw.oangle_eq_left_right

∀ {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},
  Sbtw ℝ p₁ p₂ p₁' → Sbtw ℝ p₃ p₂ p₃' → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃'

Replacing both the first and third points by ones on the same lines but the opposite rays does not change the oriented angle (vertically opposite angles).

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented