Commit 2024-11-03 08:14 283822c9

View on Github →

feat(Data/Finset/Max): max/min_union (#18545) Adds max_union and min_union as a corollary of sup_union and inf_union respectively.

Estimated changes

added theorem Finset.max_union
added theorem Finset.min_union