mathlib3 documentation

topology.omega_complete_partial_order

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 #

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

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

Equations
source
theorem Scott.is_ωSup_iff_is_lub {α : Type u} [preorder α] {c : omega_complete_partial_order.chain α} {x : α} :
Scott.is_ωSup c x ↔ is_lub (set.range ⇑c) x
source
def Scott.is_open (α : Type u) [omega_complete_partial_order α] (s : set α) :
Prop

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

Equations
source
theorem Scott.is_open_univ (α : Type u) [omega_complete_partial_order α] :
Scott.is_open α set.univ
source
theorem Scott.is_open.inter (α : Type u) [omega_complete_partial_order α] (s t : set α) :
Scott.is_open α s → Scott.is_open α t → Scott.is_open α (s ∩ t)
source
theorem Scott.is_open_sUnion (α : Type u) [omega_complete_partial_order α] (s : set (set α)) (hs : ∀ (t : set α), t ∈ s → Scott.is_open α t) :
Scott.is_open α (⋃₀ s)
source
@[reducible]
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
source
@[protected, instance]
def Scott.topological_space (α : Type u) [omega_complete_partial_order α] :
topological_space (Scott α)
Equations
source
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

Equations
source
theorem not_below_is_open {α : Type u_1} [omega_complete_partial_order α] (y : Scott α) :
is_open (not_below y)
source
theorem is_ωSup_ωSup {α : Type u_1} [omega_complete_partial_order α] (c : omega_complete_partial_order.chain α) :
Scott.is_ωSup c (omega_complete_partial_order.ωSup c)
source
theorem Scott_continuous_of_continuous {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : Scott α → Scott β) (hf : continuous f) :
omega_complete_partial_order.continuous' f
source
theorem continuous_of_Scott_continuous {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : Scott α → Scott β) (hf : omega_complete_partial_order.continuous' f) :
continuous f