Theorems · Theorem · geometry

EuclideanGeometry.angle_eq_zero_iff_eq_and_ne_or_sbtw

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁

The angle between three points is zero if and only if one of the first and third points is strictly between the other two, or those two points are equal but not equal to the second.

Defined in

Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor