Theorems · Definition · geometry

EuclideanGeometry.Sphere.power

{P : Type u_2} → [inst : MetricSpace P] → EuclideanGeometry.Sphere P → P → ℝ

The power of a point with respect to a sphere. For a point and a sphere, this is defined as the square of the distance from the point to the center minus the square of the radius. This value is positive if the point is outside the sphere, negative if inside, and zero if on the sphere.

Defined in

Mathlib.Geometry.Euclidean.Sphere.Power

Cited by

11 results in Mathlib

Foundations

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

Assumes

MetricSpace