mathlib

1330a700 - feat(data/set/intervals/disjoint): Add 4 lemmas about unions of closed semi-infinite intervals. (#17587)

feat(data/set/intervals/disjoint): Add 4 lemmas about unions of closed semi-infinite intervals. (#17587) This PR adds lemmas about unions of semi-infinite closed intervals. Lemmas about unions of semi-infinite open intervals existed. For semi-infinite closed intervals, the union depends on whether the lub or glb is included or not.