Scott continuity

A function f : α → β between preorders is Scott continuous (referring to Dana Scott) if it distributes over IsLUB. Scott continuity corresponds to continuity in Scott topological spaces (defined in Mathlib/Topology/Order/ScottTopology.lean). It is distinct from the (more commonly used) continuity from topology (see Mathlib/Topology/Basic.lean).

Implementation notes

Given a set D of directed sets, we define say f is ScottContinuousOn D if it distributes over IsLUB for all elements of D. This allows us to consider Scott Continuity on all directed sets in this file, and ωScott Continuity on chains later in Mathlib/Order/OmegaCompletePartialOrder.lean.

References

• [Abramsky and Jung, Domain Theory][abramsky_gabbay_maibaum_1994]
• [Gierz et al, A Compendium of Continuous Lattices][GierzEtAl1980]

def ScottContinuousOn {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (D : Set (Set α)) (f : α → β) : Prop

A function between preorders is said to be Scott continuous on a set D of directed sets if it preserves IsLUB on elements of D.

The dual notion

∀ ⦃d : Set α⦄, d ∈ D →  d.Nonempty → DirectedOn (· ≥ ·) d → ∀ ⦃a⦄, IsGLB d a → IsGLB (f '' d) (f a)

does not appear to play a significant role in the literature, so is omitted here.

Equations

• ScottContinuousOn D f = ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)

theorem ScottContinuousOn.mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {D₁ : Set (Set α)} {D₂ : Set (Set α)} {f : α → β} (hD : D₁ ⊆ D₂) (hf : ScottContinuousOn D₂ f) : ScottContinuousOn D₁ f

theorem ScottContinuousOn.monotone {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (D : Set (Set α)) (hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D) (h : ScottContinuousOn D f) : Monotone f

@[simp]

theorem ScottContinuousOn.id {α : Type u_1} [Preorder α] {D : Set (Set α)} : ScottContinuousOn D id

theorem ScottContinuousOn.prodMk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {D : Set (Set α)} {f : α → β} {g : α → β} (hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D) (hf : ScottContinuousOn D f) (hg : ScottContinuousOn D g) : ScottContinuousOn D fun (x : α) => (f x, g x)

def ScottContinuous {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α → β) : Prop

A function between preorders is said to be Scott continuous if it preserves IsLUB on directed sets. It can be shown that a function is Scott continuous if and only if it is continuous wrt the Scott topology.

Equations

• ScottContinuous f = ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)

@[simp]

theorem scottContinuousOn_univ {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} : ScottContinuousOn Set.univ f ↔ ScottContinuous f

theorem ScottContinuous.scottContinuousOn {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {D : Set (Set α)} : ScottContinuous f → ScottContinuousOn D f

theorem ScottContinuous.monotone {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (h : ScottContinuous f) : Monotone f

@[simp]

theorem ScottContinuous.id {α : Type u_1} [Preorder α] : ScottContinuous id

theorem ScottContinuousOn.sup₂ {β : Type u_2} [SemilatticeSup β] {D : Set (Set (β × β))} : ScottContinuousOn D fun (x : β × β) => match x with | (a, b) => a ⊔ b