Update Lex.lean

leanprover-community · Oct 31, 2024 · 531fb83 · 531fb83
1 parent 7ff3ad0
commit 531fb83
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/Mathlib/Data/Prod/Lex.lean b/Mathlib/Data/Prod/Lex.lean
@@ -50,7 +50,11 @@ theorem lt_iff [LT α] [LT β] (a b : α × β) :
     toLex a < toLex b ↔ a.1 < b.1 ∨ a.1 = b.1 ∧ a.2 < b.2 :=
   Prod.lex_def
 
-example (x : α) (y : β) : toLex (x, y) = toLex (x, y) := rfl
+theorem left_le {α β} [PartialOrder α] [LT β] {a b : α} {c d : β}
+    (h₁ : a ≤ b) (h₂ : c < d) : toLex (a, c) < toLex (b, d) := by
+  obtain h₁ | rfl := h₁.lt_or_eq
+  · exact Prod.Lex.left _ _ h₁
+  · exact Prod.Lex.right _ h₂
 
 /-- Dictionary / lexicographic preorder for pairs. -/
 instance preorder (α β : Type*) [Preorder α] [Preorder β] : Preorder (α ×ₗ β) :=