Commit 2026-03-10 19:38 6103ab78
View on Github →feat(Analysis/Convex): extremePoints ℝ (closedBall x r) ⊆ sphere x r (#35899)
... in a nontrivial normed space, with equality in a nontrivial strictly convex space.
feat(Analysis/Convex): extremePoints ℝ (closedBall x r) ⊆ sphere x r (#35899)
... in a nontrivial normed space, with equality in a nontrivial strictly convex space.