Commit 2025-03-16 18:31 dfaec4bf

View on Github →

feat: add le_sup_dite_{pos,neg}, inf_dite_{pos,neg}_le (#22445)

Estimated changes

Modified Mathlib/Data/Finset/Lattice/Fold.lean

added theorem Finset.inf_dite_neg_le

added theorem Finset.inf_dite_pos_le

added theorem Finset.le_sup_dite_neg

added theorem Finset.le_sup_dite_pos