Theorems · Theorem · geometry

EuclideanGeometry.Sphere.dist_sq_eq_mul_dist_of_tangent_and_secant

• 1000+ list: Tangent-secant theorem

∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b t p : P} {s : EuclideanGeometry.Sphere P},
  a ∈ s → b ∈ s → p ∈ line[ℝ, a, b] → s.IsTangentAt t line[ℝ, p, t] → dist p t ^ 2 = dist p a * dist p b

Tangent-Secant Theorem. The square of the tangent length equals the product of secant segment lengths.

Defined in

Mathlib.Geometry.Euclidean.Sphere.Power

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor