Theorems · Theorem · geometry

Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius

∀ {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) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        dist (t.points i₁) (t.points i₃) / |(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| /
            2 =
          Affine.Simplex.circumradius t

The circumradius of a triangle may be expressed explicitly as half the length of a side divided by the absolute value of the sine of the angle at the third point (a version of the law of sines or sine rule).

Defined in

Mathlib.Geometry.Euclidean.Angle.Sphere

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented