Theorem Finset.le_sup_dite_pos

Modification history

2025-03-16 18:31
Mathlib/Data/Finset/Lattice/Fold.lean
feat: add le_sup_dite_{pos,neg}, inf_dite_{pos,neg}_le (#22445)
Added Finset.le_sup_dite_posView on Github →