Theorems · Theorem · geometry

AffineSubspace.SOppSide.oangle_sign_eq_neg

∀ {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)]
  {s : AffineSubspace ℝ P} {p₁ p₂ p₃ p₄ : P},
  p₁ ∈ s →
    p₂ ∈ s → s.SOppSide p₃ p₄ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = -(EuclideanGeometry.oangle p₁ p₃ p₂).sign

Given two points in an affine subspace, the angles between those two points at two other points on opposite sides of that subspace have opposite signs.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented