EuclideanGeometry.Sphere.power_nonpos_iff_dist_center_le_radius
∀ {P : Type u_2} [inst : MetricSpace P] {s : EuclideanGeometry.Sphere P} {p : P},
0 ≤ s.radius → (s.power p ≤ 0 ↔ dist p s.center ≤ s.radius)The power of a point is nonpositive if and only if the point lies inside or on the sphere.
- Defined in
- Mathlib.Geometry.Euclidean.Sphere.Power
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MetricSpacestatement and proof · cited by 1,684
- Dist.diststatement and proof · cited by 1,539
- two_ne_zeroproof · cited by 251
- EuclideanGeometry.Spherestatement and proof · cited by 233
- EuclideanGeometry.Sphere.centerstatement and proof · cited by 181
- dist_nonnegproof · cited by 126
- EuclideanGeometry.Sphere.radiusstatement and proof · cited by 123
- sub_nonposproof · cited by 29
- EuclideanGeometry.Sphere.powerstatement · cited by 11
- pow_le_pow_iff_left₀proof · cited by 6
Cited by1
Results whose statement or proof uses this declaration.
- EuclideanGeometry.Sphere.mul_dist_eq_neg_power_of_dist_center_le_radiusproof · cited by 0