Commit 2025-08-04 03:44 ad58550d
View on Github →chore: golf NormedSpace.sphere_nonempty (#27910)
This result has nothing to do with pointwise operators on sets, and in finding the right file I also found a lemma which golfs it.
The motivation here was wanting this lemma in the file about operator norms.