Commit 2022-10-16 18:10 e905eeab
View on Github →feat(order/locally_finite): add lemmas expanding finset.Icc (#16996)
This avoids the need to unfold finset.Icc to access the component-wise definitions.
I only really needed this for prod, but added a handful of lemmas elsewhere too.