Lexicographic_Order_on_Products_of_Well_Ordered_Sets
Provedorder-theoryproofwiki
The lexicographic order on the product of two well-ordered sets is a well-ordering.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Order.WellFoundedSet
Formal statement
theorem Lexicographic_Order_on_Products_of_Well_Ordered_Sets {α β : Type _} [LinearOrder α] [WellFoundedLT α] [LinearOrder β] [WellFoundedLT β] : WellFoundedLT (α ×ₗ β) := by sorrySource