# mathlibdocumentation

topology.omega_complete_partial_order

# Scott Topological Spaces #

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

## Reference #

def Scott.is_ωSup {α : Type u} [preorder α] (x : α) :
Prop
Equations
def Scott.is_open (α : Type u) (s : set α) :
Prop

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

Equations
theorem Scott.is_open_univ (α : Type u)  :
theorem Scott.is_open.inter (α : Type u) (s t : set α) :
(s t)
theorem Scott.is_open_sUnion (α : Type u) (s : set (set α)) :
(∀ (t : set α), t s t) (⋃₀s)
def Scott (α : Type u) :
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
• = α
@[instance]
def Scott.topological_space (α : Type u)  :
Equations
def not_below {α : Type u_1} (y : Scott α) :
set (Scott α)

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

Equations
theorem not_below_is_open {α : Type u_1} (y : Scott α) :
theorem is_ωSup_ωSup {α : Type u_1}  :
theorem Scott_continuous_of_continuous {α : Type u_1} {β : Type u_2} (f : ) (hf : continuous f) :
theorem continuous_of_Scott_continuous {α : Type u_1} {β : Type u_2} (f : )  :