Theorems · Definition · order theory

OrderIso.ofUnique

(α : Type u_6) → (β : Type u_7) → [Unique α] → [Unique β] → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β

The order isomorphism α ≃o β when α and β are preordered types containing unique elements.

Defined in

Mathlib.Order.Hom.Basic

Cited by

3 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

UniqueUniquePreorderPreorder