# Scott Topological Spaces #

A type of topological spaces whose notion of continuity is equivalent to continuity in ωCPOs.

## Reference #

• https://ncatlab.org/nlab/show/Scott+topology
def Scott.IsωSup {α : Type u} [] (x : α) :

x is an ω-Sup of a chain c if it is the least upper bound of the range of c.

Equations
Instances For
theorem Scott.isωSup_iff_isLUB {α : Type u} [] {x : α} :
IsLUB () x
def Scott.IsOpen (α : Type u) (s : Set α) :

The characteristic function of open sets is monotone and preserves the limits of chains.

Equations
Instances For
theorem Scott.isOpen_univ (α : Type u) :
Scott.IsOpen α Set.univ
theorem Scott.IsOpen.inter (α : Type u) (s : Set α) (t : Set α) :
Scott.IsOpen α (s t)
theorem Scott.isOpen_sUnion (α : Type u) (s : Set (Set α)) (hs : ts, ) :
theorem Scott.IsOpen.isUpperSet (α : Type u) {s : Set α} (hs : ) :
@[reducible, inline]
abbrev Scott (α : Type u) :

A Scott topological space is defined on preorders such that their open sets, seen as a function α → Prop, preserves the joins of ω-chains

Equations
• = α
Instances For
instance Scott.topologicalSpace (α : Type u) :
Equations
• = { IsOpen := , isOpen_univ := , isOpen_inter := , isOpen_sUnion := }
def notBelow {α : Type u_1} (y : ) :
Set ()

notBelow is an open set in Scott α used to prove the monotonicity of continuous functions

Equations
Instances For
theorem notBelow_isOpen {α : Type u_1} (y : ) :
theorem isωSup_ωSup {α : Type u_1} :
theorem scottContinuous_of_continuous {α : Type u_1} {β : Type u_2} (f : ) (hf : ) :
theorem continuous_of_scottContinuous {α : Type u_1} {β : Type u_2} (f : ) :