power_eq_zero_iff_mem_sphere — Mathlib

English

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

Русский

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

LaTeX

$$$s.power(p)=0 \iff p\in s$$$

Lean4

/-- A point lies on the sphere if and only if its power with respect to
the sphere is zero. -/
theorem power_eq_zero_iff_mem_sphere {s : Sphere P} {p : P} (hr : 0 ≤ s.radius) : s.power p = 0 ↔ p ∈ s := by
  rw [power, mem_sphere, sub_eq_zero, pow_left_inj₀ dist_nonneg hr two_ne_zero]

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