English
UpperSet α carries a complete linear order structure, i.e., a complete lattice where the order is linear.
Русский
UpperSet α обладает полным линейным порядком; порядок линейный и полон.
LaTeX
$$$ \text{CompleteLinearOrder}(\text{UpperSet}(\alpha)) $$$
Lean4
/-- An order isomorphism of Preorders induces an order isomorphism of their lower sets. -/
def map (f : α ≃o β) : LowerSet α ≃o LowerSet β
where
toFun s := ⟨f '' s, s.lower.image f⟩
invFun t := ⟨f ⁻¹' t, t.lower.preimage f.monotone⟩
left_inv _ := SetLike.coe_injective <| f.preimage_image _
right_inv _ := SetLike.coe_injective <| f.image_preimage _
map_rel_iff' := image_subset_image_iff f.injective
