English
Let α and β be preordered sets and f: α →o β an order-preserving map. Then the induced map between the upper-set topologies on α and β is continuous; concretely, the map sending an upper set in α to its image under f defines a continuous map Topology.WithUpperSet α → Topology.WithUpperSet β.
Русский
Пусть α и β,— множества с предудалённой структурой частичного порядка, и пусть f: α →o β — монотонное отображение. Тогда полученное отображение между топологиями верхних множеств на α и β непрерывно; конкретно отображение верхнего множества в α на образ его под действием f задаёт непрерывное отображение Topology.WithUpperSet α → Topology.WithUpperSet β.
LaTeX
$$$\\forall f:\\alpha \\to_o \\beta,\\; \\mathrm{Topology.WithUpperSet.map}(f) \\text{ is a continuous map from } \\mathrm{Topology.WithUpperSet}(\\alpha) \\text{ to } \\mathrm{Topology.WithUpperSet}(\\beta).$$$
Lean4
/-- A monotone map between preorders spaces induces a continuous map between themselves considered
with the upper set topology. -/
def map (f : α →o β) : C(WithUpperSet α, WithUpperSet β)
where
toFun := toUpperSet ∘ f ∘ ofUpperSet
continuous_toFun := continuous_def.2 fun _s hs ↦ IsUpperSet.preimage hs f.monotone
