feat: port Order.LiminfLimsup (#2078)

Most notable parts of this file: - Needed to translate `isBoundedDefault` macro to lean4, very easy - Had to replace `e` with `FunLike.coe e` in a theorem statement to prevent strange coercion behaviour for Equivs.
leanprover-community · Feb 7, 2023 · 7a7c6e0 · 7a7c6e0
1 parent b00ce53
commit 7a7c6e0
Show file tree

Hide file tree

Showing 2 changed files with 1,249 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -843,6 +843,7 @@ import Mathlib.Order.InitialSeg
 import Mathlib.Order.Iterate
 import Mathlib.Order.Lattice
 import Mathlib.Order.LatticeIntervals
+import Mathlib.Order.LiminfLimsup
 import Mathlib.Order.LocallyFinite
 import Mathlib.Order.Max
 import Mathlib.Order.MinMax