feat(data/sigma/order): The lexicographical order has a bot/top (#10905)

Also fix localized instances declarations. They weren't using fully qualified names and I had forgotten `sigma.lex.linear_order`.

src/data/sigma/order.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import data.sigma.lex
+import order.bounded_order
 
 /-!
 # Orders on a sigma type
@@ -48,21 +49,23 @@ instance [Π i, partial_order (α i)] : partial_order (Σ i, α i) :=
 
 /-! ### Lexicographical order on `sigma` -/
 
+namespace lex
+
 localized "attribute [-instance] sigma.has_le" in lex
 localized "attribute [-instance] sigma.preorder" in lex
 localized "attribute [-instance] sigma.partial_order" in lex
 
 /-- The lexicographical `≤` on a sigma type. Turn this on by opening locale `lex`. -/
-def lex.has_le [has_lt ι] [Π i, has_le (α i)] : has_le (Σ i, α i) := ⟨lex (<) (λ i, (≤))⟩
+protected def has_le [has_lt ι] [Π i, has_le (α i)] : has_le (Σ i, α i) := ⟨lex (<) (λ i, (≤))⟩
 
 /-- The lexicographical `<` on a sigma type. Turn this on by opening locale `lex`. -/
-def lex.has_lt [has_lt ι] [Π i, has_lt (α i)] : has_lt (Σ i, α i) := ⟨lex (<) (λ i, (<))⟩
+protected def has_lt [has_lt ι] [Π i, has_lt (α i)] : has_lt (Σ i, α i) := ⟨lex (<) (λ i, (<))⟩
 
-localized "attribute [instance] lex.has_le" in lex
-localized "attribute [instance] lex.has_lt" in lex
+localized "attribute [instance] sigma.lex.has_le" in lex
+localized "attribute [instance] sigma.lex.has_lt" in lex
 
 /-- The lexicographical preorder on a sigma type. Turn this on by opening locale `lex`. -/
-def lex.preorder [preorder ι] [Π i, preorder (α i)] : preorder (Σ i, α i) :=
+protected def preorder [preorder ι] [Π i, preorder (α i)] : preorder (Σ i, α i) :=
 { le_refl := λ ⟨i, a⟩, lex.right a a le_rfl,
   le_trans := λ _ _ _, trans,
   lt_iff_le_not_le := begin
@@ -80,20 +83,57 @@ def lex.preorder [preorder ι] [Π i, preorder (α i)] : preorder (Σ i, α i) :
   .. lex.has_le,
   .. lex.has_lt }
 
-localized "attribute [instance] lex.preorder" in lex
+localized "attribute [instance] sigma.lex.preorder" in lex
 
 /-- The lexicographical partial order on a sigma type. Turn this on by opening locale `lex`. -/
-def lex.partial_order [preorder ι] [Π i, partial_order (α i)] : partial_order (Σ i, α i) :=
+protected def partial_order [preorder ι] [Π i, partial_order (α i)] :
+  partial_order (Σ i, α i) :=
 { le_antisymm := λ _ _, antisymm,
   .. lex.preorder }
 
-localized "attribute [instance] lex.partial_order" in lex
+localized "attribute [instance] sigma.lex.partial_order" in lex
 
 /-- The lexicographical linear order on a sigma type. Turn this on by opening locale `lex`. -/
-def lex.linear_order [linear_order ι] [Π i, linear_order (α i)] : linear_order (Σ i, α i) :=
+protected def linear_order [linear_order ι] [Π i, linear_order (α i)] :
+  linear_order (Σ i, α i) :=
 { le_total := total_of _,
   decidable_eq := sigma.decidable_eq,
   decidable_le := lex.decidable _ _,
   .. lex.partial_order }
 
+localized "attribute [instance] sigma.lex.linear_order" in lex
+
+/-- The lexicographical linear order on a sigma type. Turn this on by opening locale `lex`. -/
+protected def order_bot [partial_order ι] [order_bot ι] [Π i, preorder (α i)] [order_bot (α ⊥)] :
+  order_bot (Σ i, α i) :=
+{ bot := ⟨⊥, ⊥⟩,
+  bot_le := λ ⟨a, b⟩, begin
+    obtain rfl | ha := eq_bot_or_bot_lt a,
+    { exact lex.right _ _ bot_le },
+    { exact lex.left _ _ ha }
+  end }
+
+localized "attribute [instance] sigma.lex.order_bot" in lex
+
+/-- The lexicographical linear order on a sigma type. Turn this on by opening locale `lex`. -/
+protected def order_top [partial_order ι] [order_top ι] [Π i, preorder (α i)] [order_top (α ⊤)] :
+  order_top (Σ i, α i) :=
+{ top := ⟨⊤, ⊤⟩,
+  le_top := λ ⟨a, b⟩, begin
+    obtain rfl | ha := eq_top_or_lt_top a,
+    { exact lex.right _ _ le_top },
+    { exact lex.left _ _ ha }
+  end }
+
+localized "attribute [instance] sigma.lex.order_top" in lex
+
+/-- The lexicographical linear order on a sigma type. Turn this on by opening locale `lex`. -/
+protected def bounded_order [partial_order ι] [bounded_order ι] [Π i, preorder (α i)]
+  [order_bot (α ⊥)] [order_top (α ⊤)] :
+  bounded_order (Σ i, α i) :=
+{ .. lex.order_bot, .. lex.order_top }
+
+localized "attribute [instance] sigma.lex.bounded_order" in lex
+
+end lex
 end sigma