mathlib3

b9db1696 - chore(order/locally_finite): fill in finset interval API (#11338)

chore(order/locally_finite): fill in finset interval API (#11338) A bunch of statements about finset intervals, mimicking the set interval API and mostly proved using it. `simp` attributes are chosen as they were for sets. Also some golf. Co-authored-by: YaelDillies <yael.dillies@gmail.com>