English
The analogous identity holds for lower-set topology: the map on lower-sets induced by the identity order-hom is the identity on ContinuousMap with the lower-set topology.
Русский
Аналогично в нижнем случае: отображение, индуцируемое тот же идентичный отображение по порядку, есть тождественное непрерывное отображение на нижних множествах.
LaTeX
$$$\\mathrm{Topology.WithLowerSet.map}(\\mathrm{OrderHom.id}) = \\mathrm{ContinuousMap.id}(\\mathrm{Topology.WithLowerSet}(\\alpha)).$$$
Lean4
/-- A monotone map between preorders spaces induces a continuous map between themselves considered
with the lower set topology. -/
def map (f : α →o β) : C(WithLowerSet α, WithLowerSet β)
where
toFun := toLowerSet ∘ f ∘ ofLowerSet
continuous_toFun := continuous_def.2 fun _s hs ↦ IsLowerSet.preimage hs f.monotone
