mathlib3

ce164e28 - chore(data/{finset,multiset}/locally_finite): rename from `.interval` (#9980)

chore(data/{finset,multiset}/locally_finite): rename from `.interval` (#9980) The pattern is `data.stuff.interval` for files about `locally_finite_order stuff` and... `finset α` and `multiset α` are locally finite orders. This thus makes space for this theory.