theorem Prod.Lex.lt_iff' {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] (x y : α × β) : toLex x < toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

theorem Prod.Lex.lt_iff'' {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] (a b : Lex (α × β)) : a < b ↔ (ofLex a).1 ≤ (ofLex b).1 ∧ ((ofLex a).1 = (ofLex b).1 → (ofLex a).2 < (ofLex b).2)

instance Prod.Lex.instWellFoundedLT {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] [WellFoundedLT α] [WellFoundedLT β] : WellFoundedLT (Lex (α × β))

Equations

• ⋯ = ⋯