feat: port Order.Filter.Ultrafilter (#1814)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
leanprover-community · Jan 24, 2023 · a923247 · a923247
1 parent 66724c3
commit a923247
Show file tree

Hide file tree

Showing 2 changed files with 549 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -672,6 +672,7 @@ import Mathlib.Order.Filter.NAry
 import Mathlib.Order.Filter.Pi
 import Mathlib.Order.Filter.Prod
 import Mathlib.Order.Filter.SmallSets
+import Mathlib.Order.Filter.Ultrafilter
 import Mathlib.Order.FixedPoints
 import Mathlib.Order.GaloisConnection
 import Mathlib.Order.GameAdd