feat: port Order.WellFoundedSet (#1975)

leanprover-community · Feb 1, 2023 · 4ca8a4f · 4ca8a4f
1 parent 3e45c8e
commit 4ca8a4f
Show file tree

Hide file tree

Showing 2 changed files with 812 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -807,6 +807,7 @@ import Mathlib.Order.SupIndep
 import Mathlib.Order.SymmDiff
 import Mathlib.Order.Synonym
 import Mathlib.Order.WellFounded
+import Mathlib.Order.WellFoundedSet
 import Mathlib.Order.WithBot
 import Mathlib.Order.Zorn
 import Mathlib.Order.ZornAtoms