English
For any preorder α, there exists an order isomorphism between α and Shrink(α); in particular, α ≃o Shrink(α). The isomorphism is given by the natural equivalence equivShrink, and it preserves and reflects the order.
Русский
Для любой предкомпозиции α существует порядковый изоморфизм между α и Shrink(α); то есть α ≃o Shrink(α). Изоморфизм задаётся естественным эквивалентом equivShrink и сохраняет порядок и восстанавливает его.
LaTeX
$$$\alpha \cong_{\mathrm{ord}} \operatorname{Shrink}(\alpha)$$$
Lean4
/-- The order isomorphism `α ≃o Shrink.{u} α`. -/
noncomputable def orderIsoShrink [Preorder α] : α ≃o Shrink.{u} α
where
toEquiv := equivShrink α
map_rel_iff'
{a b} := by
obtain ⟨a, rfl⟩ := (equivShrink.{u} α).symm.surjective a
obtain ⟨b, rfl⟩ := (equivShrink.{u} α).symm.surjective b
simp only [Equiv.apply_symm_apply]
rfl
