Documentation

Mathlib.Order.Prod.Lex.Hom

Order homomorphism for Prod.Lex #

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

toLex as an OrderHom.

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