Commit 2023-03-11 18:20 f24cc289

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