mathlib3

bf07fdbb - chore(data/finset/locally_finite): add more lemmas about one-sided intervals (#17033)

chore(data/finset/locally_finite): add more lemmas about one-sided intervals (#17033) This also: * adds new `pi.locally_finite_order_bot` and `pi.locally_finite_order_top` instances, and generalizes the lemmas needed to prove things about them. * generalizes some `finsupp` lemmas about intervals to arbitrary `decidable` arguments.