mathlib3

b8858394 - refactor(data/set/intervals): Generalize `set.interval` to lattices (#17776)

refactor(data/set/intervals): Generalize `set.interval` to lattices (#17776) Replace ``` def interval (a b : α) := Icc (min a b) (max a b) ``` by ``` def interval (a b : α) := Icc (a ⊓ b) (a ⊔ b) ``` Generalize lemmas accordingly.