power — Mathlib

English

A point lies on a sphere if and only if its power equals zero, provided the radius is nonnegative.

Русский

Точка лежит на сфере тогда и только тогда, когда ее мощность равна нулю, при условии неотрицательного радиуса.

LaTeX

$$$s.power(p)=0 \Leftrightarrow p\in s$ (when $s.radius\ge 0$)$$

Lean4

/-- 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. -/
def power (s : Sphere P) (p : P) : ℝ :=
  dist p s.center ^ 2 - s.radius ^ 2

Похожие утверждения