∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β),
  UpperSet.map f =
    { toFun := fun s => { carrier := ⇑f '' ↑s, upper' := ⋯ }, invFun := fun t => { carrier := ⇑f ⁻¹' ↑t, upper' := ⋯ },
      left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }