English
There is an order isomorphism between Set(α ⊕ β) and Set α × Set β, given by s ↦ (Sum.inl^{-1}' s, Sum.inr^{-1}' s) and its inverse (A,B) ↦ Sum.inl '' A ∪ Sum.inr '' B.
Русский
Множества на сумме типов α ⊕ β эквивалентны по порядку парам множеств на α и на β: s ↦ (вперёд Sum.inl, Sum.inr) и обратное отображение.
LaTeX
$$$\mathrm{Set}(\alpha \oplus \beta) \cong_o \mathrm{Set}(\alpha) \times \mathrm{Set}(\beta)$$$
Lean4
/-- Sets on sum types are order-equivalent to pairs of sets on each summand. -/
def sumEquiv : Set (α ⊕ β) ≃o Set α × Set β
where
toFun s := (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s)
invFun s := Sum.inl '' s.1 ∪ Sum.inr '' s.2
left_inv s := image_preimage_inl_union_image_preimage_inr s
right_inv s := by simp [preimage_image_eq _ Sum.inl_injective, preimage_image_eq _ Sum.inr_injective]
map_rel_iff' := by simp [subset_def]
