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₁ 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 _root_.id

@[simp]

theorem ScottContinuousOn.fun_id {α : Type u_1} [Preorder α] {D : Set (Set α)} : ScottContinuousOn D fun (x : α) => x

Eta-expanded form of ScottContinuousOn.id

@[simp]

theorem ScottContinuousOn.const {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {D : Set (Set α)} (x : β) : ScottContinuousOn D (Function.const α x)

@[simp]

theorem ScottContinuousOn.fun_const {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {D : Set (Set α)} (x : β) : ScottContinuousOn D fun (x_1 : α) => x

Eta-expanded form of ScottContinuousOn.const

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

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

Eta-expanded form of ScottContinuousOn.comp

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

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

Eta-expanded form of ScottContinuousOn.image_comp

theorem ScottContinuousOn.prodMk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [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)

@[simp]

theorem ScottContinuousOn.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {D : Set (Set (α × β))} : ScottContinuousOn D Prod.fst

@[simp]

theorem ScottContinuousOn.snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {D : Set (Set (α × β))} : ScottContinuousOn D Prod.snd

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 w.r.t. 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 _root_.id

@[simp]

theorem ScottContinuous.fun_id {α : Type u_1} [Preorder α] : ScottContinuous fun (x : α) => x

Eta-expanded form of ScottContinuous.id

@[simp]

theorem ScottContinuous.const {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : β) : ScottContinuous (Function.const α x)

@[simp]

theorem ScottContinuous.fun_const {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : β) : ScottContinuous fun (x_1 : α) => x

Eta-expanded form of ScottContinuous.const

theorem ScottContinuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} (hf : ScottContinuous f) (hg : ScottContinuous g) : ScottContinuous (g ∘ f)

theorem ScottContinuous.fun_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} (hf : ScottContinuous f) (hg : ScottContinuous g) : ScottContinuous fun (x : α) => g (f x)

Eta-expanded form of ScottContinuous.comp

theorem ScottContinuous.prodMk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {f : α → β} {g : α → γ} (hf : ScottContinuous f) (hg : ScottContinuous g) : ScottContinuous fun (x : α) => (f x, g x)

@[simp]

theorem ScottContinuous.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : ScottContinuous Prod.fst

@[simp]

theorem ScottContinuous.snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : ScottContinuous Prod.snd

theorem ScottContinuous.sup₂ {β : Type u_2} [SemilatticeSup β] : ScottContinuous fun (b : β × β) => b.1 ⊔ b.2

The join operation is Scott continuous

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