Theorems · Theorem · geometry

EuclideanGeometry.Sphere.dist_div_cos_oangle_center_eq_two_mul_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₁ ∈ s → p₂ ∈ s → p₁ ≠ p₂ → dist p₁ p₂ / (EuclideanGeometry.oangle p₂ p₁ s.center).cos = 2 * s.radius

Given two points on a circle, twice the radius of that circle may be expressed explicitly as the distance between those two points divided by the cosine of the angle between the chord and the radius at one of those points.

Defined in

Mathlib.Geometry.Euclidean.Angle.Sphere

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorFactModule.Oriented