structure OrderHom (α : Type u_3) (β : Type u_4) [Preorder α] [Preorder β] : Type (max u_3 u_4)

• toFun : α → β

  The underlying function of an OrderHom.

• monotone : Monotone self.toFun

  The underlying function of an OrderHom is monotone.

theorem OrderHom.eq_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α →o β} : f = g ↔ f.toFun = g.toFun

def «term_→o_» : Lean.TrailingParserDescr

Equations

• «term_→o_» = Lean.ParserDescr.trailingNode `«term_→o_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →o ") (Lean.ParserDescr.cat `term 25))

instance instCoeFunOrderHomForall {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : CoeFun (α →o β) fun (x : α →o β) => α → β

Equations

• instCoeFunOrderHomForall = { coe := OrderHom.toFun }

instance instPreorderOrderHom {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : Preorder (α →o β)

Equations

• instPreorderOrderHom = Preorder.mk ⋯ ⋯ ⋯

instance instPartialOrderOrderHom {α : Type u_1} {β : Type u_2} [Preorder α] [PartialOrder β] : PartialOrder (α →o β)

Equations

• instPartialOrderOrderHom = PartialOrder.mk ⋯