Commit 2024-11-13 21:29 faca14aa

feat(Order/WellFoundedSet): sufficient conditions for unique minima of well-founded sets (#18977) This PR adds two results about minima in well-founded sets. For preorders, if an element is strictly smaller than all others, then it is equal to the minimum. For partial orders, if an element is less than or equal to all elements, then it is equal to the minimum. We add an application to the support of Hahn series.