Skip to content

Commit c2c2efa

Browse files
euprunineuprunin
committed
chore(Order/Interval/Set/LinearOrder): golf interval lemmas using grind (#31288)
1 parent 8e57b87 commit c2c2efa

File tree

3 files changed

+53
-175
lines changed

3 files changed

+53
-175
lines changed

‎Mathlib/Order/Interval/Set/Disjoint.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Floris van Doorn, Yury Kudryashov
55
-/
66
import Mathlib.Data.Set.Lattice.Image
77
import Mathlib.Order.Interval.Set.LinearOrder
8+
import Mathlib.Order.MinMax
89

910
/-!
1011
# Extra lemmas about intervals

0 commit comments

Comments
 (0)