Theorems · Theorem · geometry

EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius

∀ {V : Type u_3} {P : Type u_4} [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)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
  p₁ ∈ s →
    p₂ ∈ s →
      p₃ ∈ s → p₁ ≠ p₂ → p₁ ≠ p₃ → p₂ ≠ p₃ → dist p₁ p₃ / |(EuclideanGeometry.oangle p₁ p₂ p₃).sin| / 2 = s.radius

Given three points on a circle, the radius of that circle may be expressed explicitly as half the distance between two of those points 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 292 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented