Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-04 00:28 b031290b

View on Github →

feat(data/finset): lemmas for folding min and max (#1774) From the perfectoid project.

Estimated changes

Modified src/data/finset.lean

added theorem finset.fold_max_le

added theorem finset.fold_max_lt

added theorem finset.fold_min_le

added theorem finset.fold_min_lt

added theorem finset.fold_op_rel_iff_and

added theorem finset.fold_op_rel_iff_or

added theorem finset.le_fold_max

added theorem finset.le_fold_min

added theorem finset.lt_fold_max

added theorem finset.lt_fold_min