Commit 2025-07-15 16:28 3e077d83

View on Github →

feat: Finset.max'_eq_iff (#27153) This PR add two lemmas which give characterizations of Finset.max'/min'. (This will be used in some future cosimplicial construction.)

Estimated changes

Modified Mathlib/Data/Finset/Max.lean

added theorem Finset.max'_eq_iff

added theorem Finset.min'_eq_iff