mathlib documentation

order.category.Preorder

Category of preorders #

def Preorder  :
Type (u_1+1)

The category of preorders.

Equations
@[instance]
Equations
def Preorder.of (α : Type u_1) [preorder α] :

Construct a bundled Preorder from the underlying type and typeclass.

Equations
@[instance]
Equations