theorem Prod.lex_def {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) {p : α × β} {q : α × β} : Prod.Lex r s p q ↔ r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd

instance Prod.Lex.instDecidableRelProdLex {α : Type u_1} {β : Type u_2} [αeqDec : DecidableEq α] {r : α → α → Prop} [rDec : DecidableRel r] {s : β → β → Prop} [sDec : DecidableRel s] : DecidableRel (Prod.Lex r s)

Equations

• One or more equations did not get rendered due to their size.