English
If f: α ≃o β, then it induces an order isomorphism between the endomorphism orders: (α →o α) ≃o (β →o β).
Русский
Если f: α ≃o β, то оно индуцирует упорядоченную изоморфию между множествами самопроизводных функций: (α →o α) ≃o (β →o β).
LaTeX
$$$\text{conj}(f) : (α \to_o α) \simeq_o (β \to_o β)$ with toFun(p) = f ∘ p ∘ f^{-1}$$$
Lean4
/-- If `α` and `β` are order-isomorphic then the two orders of order-homomorphisms
from `α` and `β` to themselves are order-isomorphic. -/
@[simps! apply symm_apply]
def conj {α β} [Preorder α] [Preorder β] (f : α ≃o β) : (α →o α) ≃ (β →o β) :=
arrowCongr f f
