Theorems · Theorem · geometry

EuclideanGeometry.Sphere.IsTangentAt.power_eq_dist_sq

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

The power of a point with respect to a sphere equals the square of its tangent length.

Defined in

Mathlib.Geometry.Euclidean.Sphere.Power

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor