mathlib3 documentation


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.

Reference #

def Scott.is_ωSup {α : Type u} [preorder α] (c : omega_complete_partial_order.chain α) (x : α) :

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

def Scott.is_open (α : Type u) [omega_complete_partial_order α] (s : set α) :

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

theorem Scott.is_open_sUnion (α : Type u) [omega_complete_partial_order α] (s : set (set α)) (hs : (t : set α), t s Scott.is_open α t) :
def 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

def not_below {α : Type u_1} [omega_complete_partial_order α] (y : Scott α) :
set (Scott α)

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