feat(Finset): add IsDirected instances (#6169)

This way `IsDirected (Finset α) (· ≤ ·)` doesn't need `[DecidableEq α]`.
leanprover-community · Jul 27, 2023 · b7ec761 · b7ec761
1 parent 00269a6
commit b7ec761
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean b/Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean
@@ -48,7 +48,7 @@ def liftToFinset [HasFiniteCoproducts C] (F : Discrete α ⥤ C) : Finset (Discr
     type. -/
 @[simps!]
 def liftToFinsetColimitCocone [HasFiniteCoproducts C] [HasFilteredColimitsOfSize.{w, w} C]
-    [DecidableEq α] (F : Discrete α ⥤ C) : ColimitCocone F where
+    (F : Discrete α ⥤ C) : ColimitCocone F where
   cocone :=
     { pt := colimit (liftToFinset F)
       ι :=

diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
@@ -1849,8 +1849,10 @@ theorem disjoint_or_nonempty_inter (s t : Finset α) : Disjoint s t ∨ (s ∩ t
 
 end Lattice
 
-/-! ### erase -/
+instance isDirected_le : IsDirected (Finset α) (· ≤ ·) := by classical infer_instance
+instance isDirected_subset : IsDirected (Finset α) (· ⊆ ·) := isDirected_le
 
+/-! ### erase -/
 
 section Erase