diff --git a/Mathlib.lean b/Mathlib.lean
index a8d9d77f1d989..fa02ad7323b8a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2967,6 +2967,7 @@ import Mathlib.Order.Monotone.Extension
 import Mathlib.Order.Monotone.Monovary
 import Mathlib.Order.Monotone.Odd
 import Mathlib.Order.Monotone.Union
+import Mathlib.Order.Notation
 import Mathlib.Order.OmegaCompletePartialOrder
 import Mathlib.Order.OrdContinuous
 import Mathlib.Order.OrderIsoNat
diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
index b2d3a4b8e4e33..0997b67b64dc5 100644
--- a/Mathlib/Order/Basic.lean
+++ b/Mathlib/Order/Basic.lean
@@ -11,6 +11,7 @@ import Mathlib.Tactic.Convert
 import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.Classical
 import Mathlib.Tactic.Cases
+import Mathlib.Order.Notation
 
 #align_import order.basic from "leanprover-community/mathlib"@"90df25ded755a2cf9651ea850d1abe429b1e4eb1"
 
@@ -35,9 +36,6 @@ classes and allows to transfer order instances.
 
 ### Extra class
 
-* `Sup`: type class for the `⊔` notation
-* `Inf`: type class for the `⊓` notation
-* `HasCompl`: type class for the `ᶜ` notation
 * `DenselyOrdered`: An order with no gap, i.e. for any two elements `a < b` there exists `c` such
   that `a < c < b`.
 
@@ -794,7 +792,6 @@ end ltByCases
 
 /-! ### Order dual -/
 
-
 /-- Type synonym to equip a type with the dual order: `≤` means `≥` and `<` means `>`. `αᵒᵈ` is
 notation for `OrderDual α`. -/
 def OrderDual (α : Type*) : Type _ :=
@@ -859,18 +856,6 @@ end OrderDual
 /-! ### `HasCompl` -/
 
 
-/-- Set / lattice complement -/
-@[notation_class]
-class HasCompl (α : Type*) where
-  /-- Set / lattice complement -/
-  compl : α → α
-#align has_compl HasCompl
-
-export HasCompl (compl)
-
-@[inherit_doc]
-postfix:1024 "ᶜ" => compl
-
 instance Prop.hasCompl : HasCompl Prop :=
   ⟨Not⟩
 #align Prop.has_compl Prop.hasCompl
@@ -1077,32 +1062,8 @@ theorem max_def_lt (x y : α) : max x y = if x < y then y else x := by
 
 end MinMaxRec
 
-/-! ### `Sup` and `Inf` -/
-
-
-/-- Typeclass for the `⊔` (`\lub`) notation -/
-@[notation_class, ext]
-class Sup (α : Type u) where
-  /-- Least upper bound (`\lub` notation) -/
-  sup : α → α → α
-#align has_sup Sup
-
-/-- Typeclass for the `⊓` (`\glb`) notation -/
-@[notation_class, ext]
-class Inf (α : Type u) where
-  /-- Greatest lower bound (`\glb` notation) -/
-  inf : α → α → α
-#align has_inf Inf
-
-@[inherit_doc]
-infixl:68 " ⊔ " => Sup.sup
-
-@[inherit_doc]
-infixl:69 " ⊓ " => Inf.inf
-
 /-! ### Lifts of order instances -/
 
-
 /-- Transfer a `Preorder` on `β` to a `Preorder` on `α` using a function `f : α → β`.
 See note [reducible non-instances]. -/
 @[reducible]
diff --git a/Mathlib/Order/BoundedOrder.lean b/Mathlib/Order/BoundedOrder.lean
index 1afaa1bad8978..9462bec6f09de 100644
--- a/Mathlib/Order/BoundedOrder.lean
+++ b/Mathlib/Order/BoundedOrder.lean
@@ -40,37 +40,6 @@ variable {α : Type u} {β : Type v} {γ δ : Type*}
 
 /-! ### Top, bottom element -/
 
-
-/-- Typeclass for the `⊤` (`\top`) notation -/
-@[notation_class, ext]
-class Top (α : Type u) where
-  /-- The top (`⊤`, `\top`) element -/
-  top : α
-#align has_top Top
-
-/-- Typeclass for the `⊥` (`\bot`) notation -/
-@[notation_class, ext]
-class Bot (α : Type u) where
-  /-- The bot (`⊥`, `\bot`) element -/
-  bot : α
-#align has_bot Bot
-
-/-- The top (`⊤`, `\top`) element -/
-notation "⊤" => Top.top
-
-/-- The bot (`⊥`, `\bot`) element -/
-notation "⊥" => Bot.bot
-
-instance (priority := 100) top_nonempty (α : Type u) [Top α] : Nonempty α :=
-  ⟨⊤⟩
-#align has_top_nonempty top_nonempty
-
-instance (priority := 100) bot_nonempty (α : Type u) [Bot α] : Nonempty α :=
-  ⟨⊥⟩
-#align has_bot_nonempty bot_nonempty
-
-attribute [match_pattern] Bot.bot Top.top
-
 /-- An order is an `OrderTop` if it has a greatest element.
 We state this using a data mixin, holding the value of `⊤` and the greatest element constraint. -/
 class OrderTop (α : Type u) [LE α] extends Top α where
diff --git a/Mathlib/Order/Heyting/Basic.lean b/Mathlib/Order/Heyting/Basic.lean
index 4c520ce888cc6..aeed34d4dc541 100644
--- a/Mathlib/Order/Heyting/Basic.lean
+++ b/Mathlib/Order/Heyting/Basic.lean
@@ -33,13 +33,6 @@ Heyting algebras are the order theoretic equivalent of cartesian-closed categori
 * `CoheytingAlgebra`: Co-Heyting algebra.
 * `BiheytingAlgebra`: bi-Heyting algebra.
 
-## Notation
-
-* `⇨`: Heyting implication
-* `\`: Difference
-* `￢`: Heyting negation
-* `ᶜ`: (Pseudo-)complement
-
 ## References
 
 * [Francis Borceux, *Handbook of Categorical Algebra III*][borceux-vol3]
@@ -57,37 +50,6 @@ variable {ι α β : Type*}
 
 /-! ### Notation -/
 
-
-/-- Syntax typeclass for Heyting implication `⇨`. -/
-@[notation_class]
-class HImp (α : Type*) where
-  /-- Heyting implication `⇨` -/
-  himp : α → α → α
-#align has_himp HImp
-
-/-- Syntax typeclass for Heyting negation `￢`.
-
-The difference between `HasCompl` and `HNot` is that the former belongs to Heyting algebras,
-while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but `compl`
-underestimates while `HNot` overestimates. In boolean algebras, they are equal.
-See `hnot_eq_compl`.
--/
-@[notation_class]
-class HNot (α : Type*) where
-  /-- Heyting negation `￢` -/
-  hnot : α → α
-#align has_hnot HNot
-
-export HImp (himp)
-export SDiff (sdiff)
-export HNot (hnot)
-
-/-- Heyting implication -/
-infixr:60 " ⇨ " => himp
-
-/-- Heyting negation -/
-prefix:72 "￢" => hnot
-
 section
 variable (α β)
 
diff --git a/Mathlib/Order/Notation.lean b/Mathlib/Order/Notation.lean
new file mode 100644
index 0000000000000..858474b435184
--- /dev/null
+++ b/Mathlib/Order/Notation.lean
@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Yury Kudryashov, Yaël Dillies
+-/
+import Mathlib.Tactic.Basic
+import Mathlib.Tactic.Simps.NotationClass
+import Mathlib.Mathport.Rename
+
+/-!
+# Notation classes for lattice operations
+
+In this file we introduce typeclasses and definitions for lattice operations.
+
+## Main definitions
+
+* `Sup`: type class for the `⊔` notation
+* `Inf`: type class for the `⊓` notation
+* `HasCompl`: type class for the `ᶜ` notation
+* `Top`: type class for the `⊤` notation
+* `Bot`: type class for the `⊥` notation
+
+## Notations
+
+* `x ⊔ y`: lattice join operation;
+* `x ⊓ y`: lattice meet operation;
+* `xᶜ`: complement in a lattice;
+
+-/
+
+/-- Set / lattice complement -/
+@[notation_class]
+class HasCompl (α : Type*) where
+  /-- Set / lattice complement -/
+  compl : α → α
+#align has_compl HasCompl
+
+export HasCompl (compl)
+
+@[inherit_doc]
+postfix:1024 "ᶜ" => compl
+
+/-! ### `Sup` and `Inf` -/
+
+/-- Typeclass for the `⊔` (`\lub`) notation -/
+@[notation_class, ext]
+class Sup (α : Type*) where
+  /-- Least upper bound (`\lub` notation) -/
+  sup : α → α → α
+#align has_sup Sup
+
+/-- Typeclass for the `⊓` (`\glb`) notation -/
+@[notation_class, ext]
+class Inf (α : Type*) where
+  /-- Greatest lower bound (`\glb` notation) -/
+  inf : α → α → α
+#align has_inf Inf
+
+@[inherit_doc]
+infixl:68 " ⊔ " => Sup.sup
+
+@[inherit_doc]
+infixl:69 " ⊓ " => Inf.inf
+
+/-- Syntax typeclass for Heyting implication `⇨`. -/
+@[notation_class]
+class HImp (α : Type*) where
+  /-- Heyting implication `⇨` -/
+  himp : α → α → α
+#align has_himp HImp
+
+/-- Syntax typeclass for Heyting negation `￢`.
+
+The difference between `HasCompl` and `HNot` is that the former belongs to Heyting algebras,
+while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but `compl`
+underestimates while `HNot` overestimates. In boolean algebras, they are equal.
+See `hnot_eq_compl`.
+-/
+@[notation_class]
+class HNot (α : Type*) where
+  /-- Heyting negation `￢` -/
+  hnot : α → α
+#align has_hnot HNot
+
+export HImp (himp)
+export SDiff (sdiff)
+export HNot (hnot)
+
+/-- Heyting implication -/
+infixr:60 " ⇨ " => himp
+
+/-- Heyting negation -/
+prefix:72 "￢" => hnot
+
+
+/-- Typeclass for the `⊤` (`\top`) notation -/
+@[notation_class, ext]
+class Top (α : Type*) where
+  /-- The top (`⊤`, `\top`) element -/
+  top : α
+#align has_top Top
+
+/-- Typeclass for the `⊥` (`\bot`) notation -/
+@[notation_class, ext]
+class Bot (α : Type*) where
+  /-- The bot (`⊥`, `\bot`) element -/
+  bot : α
+#align has_bot Bot
+
+/-- The top (`⊤`, `\top`) element -/
+notation "⊤" => Top.top
+
+/-- The bot (`⊥`, `\bot`) element -/
+notation "⊥" => Bot.bot
+
+instance (priority := 100) top_nonempty (α : Type*) [Top α] : Nonempty α :=
+  ⟨⊤⟩
+#align has_top_nonempty top_nonempty
+
+instance (priority := 100) bot_nonempty (α : Type*) [Bot α] : Nonempty α :=
+  ⟨⊥⟩
+#align has_bot_nonempty bot_nonempty
+
+attribute [match_pattern] Bot.bot Top.top