Theorems · Theorem · geometry

EuclideanGeometry.cospherical_or_collinear_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] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ : P},
  2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄ →
    EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral add to π", for oriented angles mod π, with a "cospherical or collinear" conclusion.

Defined in

Mathlib.Geometry.Euclidean.Angle.Sphere

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented