Commit 2025-03-11 23:04 5fb8ff54

feat(Geometry/Euclidean/Sphere/Basic): two small lemmas (#22472) Add the following straightforward lemmas about spheres:

@[simp] lemma Sphere.center_mem_iff {s : Sphere P} : s.center ∈ s ↔ s.radius = 0 := by

lemma Sphere.nonempty_iff [Nontrivial V] {s : Sphere P} : (s : Set P).Nonempty ↔ 0 ≤ s.radius := by