English
A continuous map between topological spaces induces a monotone map between their specialization orders.
Русский
Непрерывное отображение между пространствами порождает монотонное отображение между их порядками специализации.
LaTeX
$$$\text{map}(f): \operatorname{Specialization}(\alpha) \to_o \operatorname{Specialization}(\beta)$, where $f:C(\alpha,\beta)$ and the underlying function is $toEquiv \circ f \circ ofEquiv$.$$
Lean4
/-- A continuous map between topological spaces induces a monotone map between their specialization
orders. -/
def map (f : C(α, β)) : Specialization α →o Specialization β
where
toFun := toEquiv ∘ f ∘ ofEquiv
monotone' := (map_continuous f).specialization_monotone
