Commit 2024-12-15 02:03 af60d5df
View on Github →feat: add theorems about isLUB and isGLB for Finset.sup and Finset.inf (#19961)
feat: add theorems regarding isLUB and isGLB for Finset.sup and Finset.inf
theorems were previously missing stating that Finset.sup produces a least upper bound and Finset.inf produces a greatest lower bound. This commit adds those theorems as well as the corresponding one for Finset.sup' and Finset.inf'.