Commit 2025-10-02 21:06 e793704b
View on Github →chore(Convex/Extreme): redefine IsExtreme and extremePoints (#29950)
Remove a redundant conclusion from the definitions, so that it's easier to prove these statements now.
As suggested by @YaelDillies in a comment to #23458