English
An equivalence e: α ≃ β induces an order isomorphism between Set α and Set β by s ↦ e''s, with inverse s ↦ e.symm''s.
Русский
Эквивалентность e: α ≃ β порождает упорядоченную изоморфию между Set α и Set β, заданную s ↦ e''s, обратное — e.symm''s.
LaTeX
$$$$ \mathrm{toOrderIsoSet}(e) : \mathrm{Set}(\alpha) \cong_o \mathrm{Set}(\beta). $$$$
Lean4
/-- An equivalence of types yields an order isomorphism between their lattices of subsets. -/
@[simps]
def toOrderIsoSet (e : α ≃ β) : Set α ≃o Set β where
toFun s := e '' s
invFun s := e.symm '' s
left_inv s := by simp only [← image_comp, Equiv.symm_comp_self, id, image_id']
right_inv s := by simp only [← image_comp, Equiv.self_comp_symm, id, image_id']
map_rel_iff' := ⟨fun h => by simpa using @monotone_image _ _ e.symm _ _ h, fun h => monotone_image h⟩
