mathlib3

94379028 - refactor(data/set/pointwise/interval): split (#17873)

refactor(data/set/pointwise/interval): split (#17873) * Extract `data.set.interval.monoid` from `data.set.pointwise.interval`. * Import it in `data.finset.locally_finite`, golf some proofs. * Add `finset.map_add_left_Icc` etc.