Theorems · Theorem · geometry

Affine.Triangle.dist_div_sin_oangle_eq_two_mul_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

Twice the circumradius of a triangle may be expressed explicitly as 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

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented