mathlib

f24cc289 - chore(data/finset/locally_finite): lemmas about open intervals (#18533)

chore(data/finset/locally_finite): lemmas about open intervals (#18533) We had `cons` lemmas for the other four cases, but not these two. The new lemmas golf a proof a little. Also adds some docstrings to makes these lemmas easier to find. Forward-ported in https://github.com/leanprover-community/mathlib4/pull/2812