basic): add `finset.piecewise_le_piecewise` (#5572)

Commit

5 years ago

feat(data/finset/basic): add `finset.piecewise_le_piecewise` (#5572) * add `finset.piecewise_le_piecewise` and `finset.piecewise_le_piecewise'`; * add `finset.piecewise_compl`.

Author

urkud

Parents

0a4fbd8c

mathlib3 9fc7aa56 - feat(data/finset/basic): add `finset.piecewise_le_piecewise` (#5572)

mathlib3
9fc7aa56 - feat(data/finset/basic): add `finset.piecewise_le_piecewise` (#5572)