Theorems · Theorem · geometry

AffineSubspace.SSameSide.oangle_sign_eq

∀ {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.SSameSide 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 the same side of that subspace have the same sign.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented