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

@[simp]

theorem Topology.IsScott.ωscottContinuous_iff_continuous {α : Type u_1} [OmegaCompletePartialOrder α] [TopologicalSpace α] [Topology.IsScott α (Set.range fun (c : OmegaCompletePartialOrder.Chain α) => Set.range ⇑c)] {f : α → Prop} : OmegaCompletePartialOrder.ωScottContinuous f ↔ Continuous f

def Scott.IsωSup {α : Type u} [Preorder α] (c : OmegaCompletePartialOrder.Chain α) (x : α) : Prop

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

Equations

• Scott.IsωSup c x = ((∀ (i : ℕ), c i ≤ x) ∧ ∀ (y : α), (∀ (i : ℕ), c i ≤ y) → x ≤ y)

theorem Scott.isωSup_iff_isLUB {α : Type u} [Preorder α] {c : OmegaCompletePartialOrder.Chain α} {x : α} : Scott.IsωSup c x ↔ IsLUB (Set.range ⇑c) x

def Scott.IsOpen (α : Type u) [OmegaCompletePartialOrder α] (s : Set α) : Prop

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

Equations

• Scott.IsOpen α s = OmegaCompletePartialOrder.ωScottContinuous fun (x : α) => x ∈ s

theorem Scott.isOpen_univ (α : Type u) [OmegaCompletePartialOrder α] : Scott.IsOpen α Set.univ

theorem Scott.IsOpen.inter (α : Type u) [OmegaCompletePartialOrder α] (s t : Set α) : Scott.IsOpen α s → Scott.IsOpen α t → Scott.IsOpen α (s ∩ t)

theorem Scott.isOpen_sUnion (α : Type u) [OmegaCompletePartialOrder α] (s : Set (Set α)) (hs : ∀ t ∈ s, Scott.IsOpen α t) : Scott.IsOpen α (⋃₀ s)

theorem Scott.IsOpen.isUpperSet (α : Type u) [OmegaCompletePartialOrder α] {s : Set α} (hs : Scott.IsOpen α s) : IsUpperSet s

@[reducible, inline]

abbrev 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

• Scott α = α

instance Scott.topologicalSpace (α : Type u) [OmegaCompletePartialOrder α] : TopologicalSpace (Scott α)

Equations

• Scott.topologicalSpace α = { IsOpen := Scott.IsOpen α, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

theorem isOpen_iff_ωScottContinuous_mem {α : Type u_1} [OmegaCompletePartialOrder α] {s : Set (Scott α)} : IsOpen s ↔ OmegaCompletePartialOrder.ωScottContinuous fun (x : Scott α) => x ∈ s

theorem scott_eq_Scott {α : Type u_1} [OmegaCompletePartialOrder α] : Topology.scott α (Set.range fun (c : OmegaCompletePartialOrder.Chain α) => Set.range ⇑c) = Scott.topologicalSpace α

def notBelow {α : Type u_1} [OmegaCompletePartialOrder α] (y : Scott α) : Set (Scott α)

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

Equations

• notBelow y = {x : Scott α | ¬x ≤ y}

theorem notBelow_isOpen {α : Type u_1} [OmegaCompletePartialOrder α] (y : Scott α) : IsOpen (notBelow y)

theorem isωSup_ωSup {α : Type u_1} [OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α) : Scott.IsωSup c (OmegaCompletePartialOrder.ωSup c)

theorem scottContinuous_of_continuous {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : Scott α → Scott β) (hf : Continuous f) : OmegaCompletePartialOrder.ωScottContinuous f

theorem continuous_of_scottContinuous {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : Scott α → Scott β) (hf : OmegaCompletePartialOrder.ωScottContinuous f) : Continuous f