mathlib3

3e88bb32 - chore(data/finset/locally_finite): add more lemmas about one-sided intervals