mathlib documentation

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 α] :

Equations
def Scott.is_open (α : Type u) [omega_complete_partial_order α] :
set α → Prop

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

Equations
theorem Scott.is_open_inter (α : Type u) [omega_complete_partial_order α] (s t : set α) :
Scott.is_open α sScott.is_open α tScott.is_open α (s t)

theorem Scott.is_open_sUnion (α : Type u) [omega_complete_partial_order α] (s : set (set α)) :
(∀ (t : set α), t sScott.is_open α t)Scott.is_open α (⋃₀s)

def Scott  :
Type uType 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
def not_below {α : Type u_1} [omega_complete_partial_order α] :
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} [omega_complete_partial_order α] (y : Scott α) :