feat: port Order.Hom.Bounded (#888)

mathlib3 SHA : f1a2caaf51ef593799107fe9a8d5e411599f3996 Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
leanprover-community · Jan 17, 2023 · afa1900 · afa1900
1 parent f20a2b3
commit afa1900
Show file tree

Hide file tree

Showing 2 changed files with 830 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -566,6 +566,7 @@ import Mathlib.Order.Heyting.Basic
 import Mathlib.Order.Heyting.Boundary
 import Mathlib.Order.Heyting.Regular
 import Mathlib.Order.Hom.Basic
+import Mathlib.Order.Hom.Bounded
 import Mathlib.Order.Hom.Order
 import Mathlib.Order.Hom.Set
 import Mathlib.Order.InitialSeg