Commit 2022-12-14 05:27 b8858394
View on Github →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.