English
A functor between preorder categories is monotone on objects; this is a standard property of monotone functors.
Русский
Функтор между категориями порядков монотонен по объектам.
LaTeX
$$Theorem: Monotone f.obj, where f : X ⥤ Y.$$
Lean4
/-- A categorical equivalence between partial orders is just an order isomorphism. -/
def toOrderIso (e : X ≌ Y) : X ≃o Y where
toFun := e.functor.obj
invFun := e.inverse.obj
left_inv a := (e.unitIso.app a).to_eq.symm
right_inv b := (e.counitIso.app b).to_eq
map_rel_iff'
{a
a'} :=
⟨fun h => ((Equivalence.unit e).app a ≫ e.inverse.map h.hom ≫ (Equivalence.unitInv e).app a').le, fun h : a ≤ a' =>
(e.functor.map h.hom).le⟩
-- `@[simps]` on `Equivalence.toOrderIso` produces lemmas that fail the `simpNF` linter,
-- so we provide them by hand:
