chore(Order/Bounds): move defs to a new file (#17676)

Also generalize definitions to `LE`.

Mathlib.lean

@@ -3571,6 +3571,7 @@ import Mathlib.Order.Booleanisation
 import Mathlib.Order.Bounded
 import Mathlib.Order.BoundedOrder
 import Mathlib.Order.Bounds.Basic
+import Mathlib.Order.Bounds.Defs
 import Mathlib.Order.Bounds.OrderIso
 import Mathlib.Order.Category.BddDistLat
 import Mathlib.Order.Category.BddLat

Mathlib/Algebra/CharP/Defs.lean

@@ -12,6 +12,7 @@ import Mathlib.Data.Nat.Find
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.ULift
 import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Order.Interval.Set.Basic
 
 /-!
 # Characteristic of semirings

Mathlib/Data/Int/GCD.lean

@@ -7,7 +7,9 @@ import Mathlib.Algebra.Group.Int
 import Mathlib.Algebra.GroupWithZero.Semiconj
 import Mathlib.Algebra.Group.Commute.Units
 import Mathlib.Data.Nat.GCD.Basic
-import Mathlib.Order.Bounds.Basic
+import Mathlib.Order.Lattice
+import Mathlib.Data.Set.Operations
+import Mathlib.Order.Bounds.Defs
 
 /-!
 # Extended GCD and divisibility over ℤ

Mathlib/Order/Bounds/Basic.lean

@@ -3,26 +3,19 @@ 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
 -/
-import Mathlib.Order.Interval.Set.Basic
 import Mathlib.Data.Set.NAry
+import Mathlib.Order.Bounds.Defs
 import Mathlib.Order.Directed
+import Mathlib.Order.Interval.Set.Basic
 
 /-!
 # Upper / lower bounds
 
-In this file we define:
-* `upperBounds`, `lowerBounds` : the set of upper bounds (resp., lower bounds) of a set;
-* `BddAbove s`, `BddBelow s` : the set `s` is bounded above (resp., below), i.e., the set of upper
-  (resp., lower) bounds of `s` is nonempty;
-* `IsLeast s a`, `IsGreatest s a` : `a` is a least (resp., greatest) element of `s`;
-  for a partial order, it is unique if exists;
-* `IsLUB s a`, `IsGLB s a` : `a` is a least upper bound (resp., a greatest lower bound)
-  of `s`; for a partial order, it is unique if exists.
-We also prove various lemmas about monotonicity, behaviour under `∪`, `∩`, `insert`, and provide
-formulas for `∅`, `univ`, and intervals.
+In this file we prove various lemmas about upper/lower bounds of a set:
+monotonicity, behaviour under `∪`, `∩`, `insert`,
+and provide formulas for `∅`, `univ`, and intervals.
 -/
 
-
 open Function Set
 
 open OrderDual (toDual ofDual)
@@ -35,43 +28,6 @@ section
 
 variable [Preorder α] [Preorder β] {s t : Set α} {a b : α}
 
-/-!
-### Definitions
--/
-
-
-/-- The set of upper bounds of a set. -/
-def upperBounds (s : Set α) : Set α :=
-  { x | ∀ ⦃a⦄, a ∈ s → a ≤ x }
-
-/-- The set of lower bounds of a set. -/
-def lowerBounds (s : Set α) : Set α :=
-  { x | ∀ ⦃a⦄, a ∈ s → x ≤ a }
-
-/-- A set is bounded above if there exists an upper bound. -/
-def BddAbove (s : Set α) :=
-  (upperBounds s).Nonempty
-
-/-- A set is bounded below if there exists a lower bound. -/
-def BddBelow (s : Set α) :=
-  (lowerBounds s).Nonempty
-
-/-- `a` is a least element of a set `s`; for a partial order, it is unique if exists. -/
-def IsLeast (s : Set α) (a : α) : Prop :=
-  a ∈ s ∧ a ∈ lowerBounds s
-
-/-- `a` is a greatest element of a set `s`; for a partial order, it is unique if exists. -/
-def IsGreatest (s : Set α) (a : α) : Prop :=
-  a ∈ s ∧ a ∈ upperBounds s
-
-/-- `a` is a least upper bound of a set `s`; for a partial order, it is unique if exists. -/
-def IsLUB (s : Set α) : α → Prop :=
-  IsLeast (upperBounds s)
-
-/-- `a` is a greatest lower bound of a set `s`; for a partial order, it is unique if exists. -/
-def IsGLB (s : Set α) : α → Prop :=
-  IsGreatest (lowerBounds s)
-
 theorem mem_upperBounds : a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a :=
   Iff.rfl
 

Mathlib/Order/Bounds/Defs.lean

@@ -0,0 +1,55 @@
+/-
+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
+-/
+import Mathlib.Data.Set.Defs
+import Mathlib.Tactic.TypeStar
+
+/-!
+# Definitions about upper/lower bounds
+
+In this file we define:
+* `upperBounds`, `lowerBounds` : the set of upper bounds (resp., lower bounds) of a set;
+* `BddAbove s`, `BddBelow s` : the set `s` is bounded above (resp., below), i.e., the set of upper
+  (resp., lower) bounds of `s` is nonempty;
+* `IsLeast s a`, `IsGreatest s a` : `a` is a least (resp., greatest) element of `s`;
+  for a partial order, it is unique if exists;
+* `IsLUB s a`, `IsGLB s a` : `a` is a least upper bound (resp., a greatest lower bound)
+  of `s`; for a partial order, it is unique if exists.
+-/
+
+variable {α : Type*} [LE α]
+
+/-- The set of upper bounds of a set. -/
+def upperBounds (s : Set α) : Set α :=
+  { x | ∀ ⦃a⦄, a ∈ s → a ≤ x }
+
+/-- The set of lower bounds of a set. -/
+def lowerBounds (s : Set α) : Set α :=
+  { x | ∀ ⦃a⦄, a ∈ s → x ≤ a }
+
+/-- A set is bounded above if there exists an upper bound. -/
+def BddAbove (s : Set α) :=
+  (upperBounds s).Nonempty
+
+/-- A set is bounded below if there exists a lower bound. -/
+def BddBelow (s : Set α) :=
+  (lowerBounds s).Nonempty
+
+/-- `a` is a least element of a set `s`; for a partial order, it is unique if exists. -/
+def IsLeast (s : Set α) (a : α) : Prop :=
+  a ∈ s ∧ a ∈ lowerBounds s
+
+/-- `a` is a greatest element of a set `s`; for a partial order, it is unique if exists. -/
+def IsGreatest (s : Set α) (a : α) : Prop :=
+  a ∈ s ∧ a ∈ upperBounds s
+
+/-- `a` is a least upper bound of a set `s`; for a partial order, it is unique if exists. -/
+def IsLUB (s : Set α) : α → Prop :=
+  IsLeast (upperBounds s)
+
+/-- `a` is a greatest lower bound of a set `s`; for a partial order, it is unique if exists. -/
+def IsGLB (s : Set α) : α → Prop :=
+  IsGreatest (lowerBounds s)
+

Mathlib/Order/WellFounded.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Data.Set.Function
-import Mathlib.Order.Bounds.Basic
+import Mathlib.Order.Bounds.Defs
 
 /-!
 # Well-founded relations