Theorems · Theorem · geometry

EuclideanGeometry.dist_eq_of_two_zsmul_oangle_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] [inst_4 : Module.Oriented ℝ V (Fin 2)] [inst_5 : Fact (Module.finrank ℝ V = 2)]
  {p₁ p₂ p₃ : P},
  2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₂ p₃ p₁ →
    EuclideanGeometry.oangle p₃ p₁ p₂ ≠ 0 → EuclideanGeometry.oangle p₃ p₁ p₂ ≠ ↑Real.pi → dist p₁ p₂ = dist p₁ p₃

Converse of pons asinorum, oriented angle-at-point form (given equality of angles mod π).

Defined in

Mathlib.Geometry.Euclidean.Triangle

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorModule.OrientedFact