Order homomorphism for Prod.Lex

def Prod.Lex.toLexOrderHom {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] : α × β →o Lex (α × β)

toLex as an OrderHom.

Equations

• Prod.Lex.toLexOrderHom = { toFun := ⇑toLex, monotone' := ⋯ }

@[simp]

theorem Prod.Lex.toLexOrderHom_coe {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] (a : α × β) : toLexOrderHom a = toLex a