Theorem EuclideanGeometry.Sphere.nonempty_iff

Modification history

2025-03-11 23:04
Mathlib/Geometry/Euclidean/Sphere/Basic.lean
feat(Geometry/Euclidean/Sphere/Basic): two small lemmas (#22472) …
Added EuclideanGeometry.Sphere.nonempty_iffView on Github →