Theorem EuclideanGeometry.Sphere.dist_center_midpoint_lt_radius

Modification history

2026-03-10 12:02
Mathlib/Geometry/Euclidean/Sphere/Basic.lean
feat: add dist_center_midpoint_lt_radius for spheres (#35957) …
Added EuclideanGeometry.Sphere.dist_center_midpoint_lt_radiusView on Github →