mathlib

e905eeab - feat(order/locally_finite): add lemmas expanding `finset.Icc` (#16996)

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.