power_pos_iff_radius_lt_dist_center

English

Power of a point is positive iff the point lies outside the sphere; it is nonnegative iff the point lies outside or on the sphere; negative iff inside.

Русский

Мощность точки положительная тогда, когда точка лежит вне сферы; неотрицательная — вне сферы или на ней; отрицательная — внутри.

LaTeX

$$0 < s.power(p) \Leftrightarrow dist(p,s.center) > s.radius$$

Lean4

/-- The power of a point is positive if and only if the point lies outside the sphere. -/
theorem power_pos_iff_radius_lt_dist_center {s : Sphere P} {p : P} (hr : 0 ≤ s.radius) :
    0 < s.power p ↔ s.radius < dist p s.center := by
  rw [power, sub_pos, pow_lt_pow_iff_left₀ hr dist_nonneg two_ne_zero]

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