Scott Topological Spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
A type of topological spaces whose notion
of continuity is equivalent to continuity in ωCPOs.
x is an
ω-Sup of a chain
c if it is the least upper bound of the range of
The characteristic function of open sets is monotone and preserves
the limits of chains.
A Scott topological space is defined on preorders
such that their open sets, seen as a function
α → Prop,
preserves the joins of ω-chains
not_below is an open set in
Scott α used
to prove the monotonicity of continuous functions