Theorems · Theorem · geometry

Affine.Triangle.mem_circumsphere_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)]
  {t : Affine.Triangle ℝ P} {p : P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        2 • EuclideanGeometry.oangle (t.points i₁) p (t.points i₃) =
            2 • EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃) →
          p ∈ Affine.Simplex.circumsphere t

Given a triangle, and a fourth point such that twice the angle between two points of the triangle at that fourth point equals twice the third angle of the triangle, the fourth point lies in the circumsphere of the triangle.

Defined in

Mathlib.Geometry.Euclidean.Angle.Sphere

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented