English
The map construction sends an order isomorphism f: α ≃o β to an order isomorphism between UpperSet α and UpperSet β by s ↦ ⟨f''s, s.upper.image f⟩.
Русский
Произведение отображения по изоморфизму порядка f: α ≃o β задаёт отображение между верхними множествами: s ↦ ⟨f''s, s.upper.image f⟩.
LaTeX
$$$\text{map}(f): \text{UpperSet}(\alpha) \to \text{UpperSet}(\beta),\quad \text{toFun}(s) = \langle f''s, s.upper.image f\rangle.$$$
Lean4
/-- An order isomorphism of Preorders induces an order isomorphism of their upper sets. -/
def map (f : α ≃o β) : UpperSet α ≃o UpperSet β
where
toFun s := ⟨f '' s, s.upper.image f⟩
invFun t := ⟨f ⁻¹' t, t.upper.preimage f.monotone⟩
left_inv _ := ext <| f.preimage_image _
right_inv _ := ext <| f.image_preimage _
map_rel_iff' := image_subset_image_iff f.injective
