feat: port Order.Filter.Germ (#1799)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com>
leanprover-community · Feb 15, 2023 · c8bff08 · c8bff08
1 parent 8609239
commit c8bff08
Show file tree

Hide file tree

Showing 2 changed files with 725 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -866,6 +866,7 @@ import Mathlib.Order.Filter.Cofinite
 import Mathlib.Order.Filter.CountableInter
 import Mathlib.Order.Filter.Curry
 import Mathlib.Order.Filter.Extr
+import Mathlib.Order.Filter.Germ
 import Mathlib.Order.Filter.IndicatorFunction
 import Mathlib.Order.Filter.Interval
 import Mathlib.Order.Filter.Lift