# mathlibdocumentation

order.omega_complete_partial_order

# Omega Complete Partial Orders #

An omega-complete partial order is a partial order with a supremum operation on increasing sequences indexed by natural numbers (which we call ωSup). In this sense, it is strictly weaker than join complete semi-lattices as only ω-sized totally ordered sets have a supremum.

The concept of an omega-complete partial order (ωCPO) is useful for the formalization of the semantics of programming languages. Its notion of supremum helps define the meaning of recursive procedures.

## Main definitions #

• class omega_complete_partial_order
• ite, map, bind, seq as continuous morphisms

## Instances of omega_complete_partial_order#

• part
• every complete_lattice
• pi-types
• product types
• monotone_hom
• continuous_hom (with notation →𝒄)
• an instance of omega_complete_partial_order (α →𝒄 β)
• continuous_hom.of_fun
• continuous_hom.of_mono
• continuous functions:
• id
• ite
• const
• part.bind
• part.map
• part.seq

## References #

def order_hom.bind {α : Type u_1} [preorder α] {β γ : Type u_2} (f : α →o part β) (g : α →o β → part γ) :
α →o part γ

part.bind as a monotone function

Equations
@[simp]
theorem order_hom.bind_coe {α : Type u_1} [preorder α] {β γ : Type u_2} (f : α →o part β) (g : α →o β → part γ) (x : α) :
(f.bind g) x = f x >>= g x
def omega_complete_partial_order.chain (α : Type u) [preorder α] :
Type u

A chain is a monotone sequence.

See the definition on page 114 of [Gun92].

Equations
Instances for omega_complete_partial_order.chain
@[protected, instance]
def omega_complete_partial_order.chain.has_coe_to_fun {α : Type u} [preorder α] :
(λ (_x : , → α)
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def omega_complete_partial_order.chain.map {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α →o β) :

map function for chain

Equations
@[simp]
theorem omega_complete_partial_order.chain.map_coe {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α →o β) :
(c.map f) = f c
theorem omega_complete_partial_order.chain.mem_map {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α →o β} (x : α) :
x cf x c.map f
theorem omega_complete_partial_order.chain.exists_of_mem_map {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α →o β} {b : β} :
b c.map f(∃ (a : α), a c f a = b)
theorem omega_complete_partial_order.chain.mem_map_iff {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α →o β} {b : β} :
b c.map f ∃ (a : α), a c f a = b
@[simp]
theorem omega_complete_partial_order.chain.map_id {α : Type u} [preorder α]  :
= c
theorem omega_complete_partial_order.chain.map_comp {α : Type u} {β : Type v} {γ : Type u_1} [preorder α] [preorder β] [preorder γ] {f : α →o β} (g : β →o γ) :
(c.map f).map g = c.map (g.comp f)
theorem omega_complete_partial_order.chain.map_le_map {α : Type u} {β : Type v} [preorder α] [preorder β] {f g : α →o β} (h : f g) :
c.map f c.map g
def omega_complete_partial_order.chain.zip {α : Type u} {β : Type v} [preorder α] [preorder β]  :

chain.zip pairs up the elements of two chains that have the same index

Equations
• c₀.zip c₁ = c₁
@[simp]
theorem omega_complete_partial_order.chain.zip_coe {α : Type u} {β : Type v} [preorder α] [preorder β] (x : ) :
(c₀.zip c₁) x = (c₀ x, c₁ x)
@[class]
structure omega_complete_partial_order (α : Type u_1) :
Type u_1
• to_partial_order :
• ωSup :
• le_ωSup : ∀ (c : (i : ),
• ωSup_le : ∀ (c : (x : α), (∀ (i : ), c i x)

An omega-complete partial order is a partial order with a supremum operation on increasing sequences indexed by natural numbers (which we call ωSup). In this sense, it is strictly weaker than join complete semi-lattices as only ω-sized totally ordered sets have a supremum.

See the definition on page 114 of [Gun92].

Instances of this typeclass
Instances of other typeclasses for omega_complete_partial_order
• omega_complete_partial_order.has_sizeof_inst
@[protected, reducible]
def omega_complete_partial_order.lift {α : Type u} {β : Type v} (f : β →o α) (ωSup₀ : → β) (h : ∀ (x y : β), f x f yx y) (h' : ∀ (c : , f (ωSup₀ c) = ) :

Transfer a omega_complete_partial_order on β to a omega_complete_partial_order on α using a strictly monotone function f : β →o α, a definition of ωSup and a proof that f is continuous with regard to the provided ωSup and the ωCPO on α.

Equations
theorem omega_complete_partial_order.le_ωSup_of_le {α : Type u} {x : α} (i : ) (h : x c i) :
theorem omega_complete_partial_order.ωSup_total {α : Type u} {x : α} (h : ∀ (i : ), c i x x c i) :
theorem omega_complete_partial_order.ωSup_le_ωSup_of_le {α : Type u} {c₀ c₁ : omega_complete_partial_order.chain α} (h : c₀ c₁) :
theorem omega_complete_partial_order.ωSup_le_iff {α : Type u} (x : α) :
∀ (i : ), c i x
def omega_complete_partial_order.subtype {α : Type u_1} (p : α → Prop) (hp : ∀ (c : , (∀ (i : α), i cp i)) :

A subset p : α → Prop of the type closed under ωSup induces an omega_complete_partial_order on the subtype {a : α // p a}.

Equations
def omega_complete_partial_order.continuous {α : Type u} {β : Type v} (f : α →o β) :
Prop

A monotone function f : α →o β is continuous if it distributes over ωSup.

In order to distinguish it from the (more commonly used) continuity from topology (see topology/basic.lean), the present definition is often referred to as "Scott-continuity" (referring to Dana Scott). It corresponds to continuity in Scott topological spaces (not defined here).

Equations
def omega_complete_partial_order.continuous' {α : Type u} {β : Type v} (f : α → β) :
Prop

continuous' f asserts that f is both monotone and continuous.

Equations
theorem omega_complete_partial_order.continuous'.to_monotone {α : Type u} {β : Type v} {f : α → β}  :
theorem omega_complete_partial_order.continuous.of_bundled {α : Type u} {β : Type v} (f : α → β) (hf : monotone f) (hf' : omega_complete_partial_order.continuous {to_fun := f, monotone' := hf}) :
theorem omega_complete_partial_order.continuous.of_bundled' {α : Type u} {β : Type v} (f : α →o β)  :
theorem omega_complete_partial_order.continuous'.to_bundled {α : Type u} {β : Type v} (f : α → β)  :
@[simp, norm_cast]
theorem omega_complete_partial_order.continuous'_coe {α : Type u} {β : Type v} {f : α →o β} :
theorem omega_complete_partial_order.continuous_comp {α : Type u} {β : Type v} {γ : Type u_1} (f : α →o β) (g : β →o γ)  :
theorem omega_complete_partial_order.continuous_const {α : Type u} {β : Type v} (x : β) :
theorem omega_complete_partial_order.const_continuous' {α : Type u} {β : Type v} (x : β) :
theorem part.eq_of_chain {α : Type u} {a b : α} (ha : c) (hb : c) :
a = b
@[protected]
noncomputable def part.ωSup {α : Type u}  :
part α

The (noncomputable) ωSup definition for the ω-CPO structure on part α.

Equations
theorem part.ωSup_eq_some {α : Type u} {a : α} (h : c) :
theorem part.ωSup_eq_none {α : Type u} (h : ¬∃ (a : α), c) :
theorem part.mem_chain_of_mem_ωSup {α : Type u} {a : α} (h : a ) :
c
@[protected, instance]
noncomputable def part.omega_complete_partial_order {α : Type u} :
Equations
theorem part.mem_ωSup {α : Type u} (x : α)  :
@[protected, instance]
def pi.omega_complete_partial_order {α : Type u_1} {β : α → Type u_2} [Π (a : α), ] :
omega_complete_partial_order (Π (a : α), β a)
Equations
theorem pi.omega_complete_partial_order.flip₁_continuous' {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [Π (x : α), ] (f : Π (x : α), γ → β x) (a : α) (hf : omega_complete_partial_order.continuous' (λ (x : γ) (y : α), f y x)) :
theorem pi.omega_complete_partial_order.flip₂_continuous' {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [Π (x : α), ] (f : γ → Π (x : α), β x) (hf : ∀ (x : α), omega_complete_partial_order.continuous' (λ (g : γ), f g x)) :
@[simp]
theorem prod.ωSup_snd {α : Type u_1} {β : Type u_2} (c : omega_complete_partial_order.chain × β)) :
@[simp]
theorem prod.ωSup_fst {α : Type u_1} {β : Type u_2} (c : omega_complete_partial_order.chain × β)) :
@[protected]
def prod.ωSup {α : Type u_1} {β : Type u_2} (c : omega_complete_partial_order.chain × β)) :
α × β

The supremum of a chain in the product ω-CPO.

Equations
@[simp]
theorem prod.omega_complete_partial_order_ωSup_fst {α : Type u_1} {β : Type u_2} (c : omega_complete_partial_order.chain × β)) :
@[simp]
theorem prod.omega_complete_partial_order_ωSup_snd {α : Type u_1} {β : Type u_2} (c : omega_complete_partial_order.chain × β)) :
@[protected, instance]
def prod.omega_complete_partial_order {α : Type u_1} {β : Type u_2}  :
Equations
theorem prod.ωSup_zip {α : Type u_1} {β : Type u_2}  :
@[protected, instance]

Any complete lattice has an ω-CPO structure where the countable supremum is a special case of arbitrary suprema.

Equations
theorem complete_lattice.Sup_continuous {α : Type u} {β : Type v} (s : set →o β)) (hs : ∀ (f : α →o β), ) :
theorem complete_lattice.supr_continuous {α : Type u} {β : Type v} {ι : Sort u_1} {f : ι → α →o β} (h : ∀ (i : ι), ) :
theorem complete_lattice.Sup_continuous' {α : Type u} {β : Type v} (s : set (α → β)) (hc : ∀ (f : α → β), ) :
theorem complete_lattice.sup_continuous {α : Type u} {β : Type v} {f g : α →o β}  :
theorem complete_lattice.top_continuous {α : Type u} {β : Type v}  :
theorem complete_lattice.bot_continuous {α : Type u} {β : Type v}  :
theorem complete_lattice.inf_continuous {α : Type u_1} {β : Type u_2} (f g : α →o β)  :
theorem complete_lattice.inf_continuous' {α : Type u_1} {β : Type u_2} {f g : α → β}  :
@[protected]
def omega_complete_partial_order.order_hom.ωSup {α : Type u} {β : Type v} (c : omega_complete_partial_order.chain →o β)) :
α →o β

The ωSup operator for monotone functions.

Equations
@[simp]
theorem omega_complete_partial_order.order_hom.ωSup_coe {α : Type u} {β : Type v} (c : omega_complete_partial_order.chain →o β)) (a : α) :
@[protected, instance]
Equations
structure omega_complete_partial_order.continuous_hom (α : Type u) (β : Type v)  :
Type (max u v)
• to_order_hom : α →o β
• cont :

A monotone function on ω-continuous partial orders is said to be continuous if for every chain c : chain α, f (⊔ i, c i) = ⊔ i, f (c i). This is just the bundled version of order_hom.continuous.

Instances for omega_complete_partial_order.continuous_hom
@[protected, instance]
def omega_complete_partial_order.continuous_hom.has_coe_to_fun (α : Type u) (β : Type v)  :
has_coe_to_fun →𝒄 β) (λ (_x : α →𝒄 β), α → β)
Equations
@[protected, instance]
def omega_complete_partial_order.order_hom.has_coe (α : Type u) (β : Type v)  :
has_coe →𝒄 β) →o β)
Equations
@[protected, instance]
Equations
def omega_complete_partial_order.continuous_hom.simps.apply (α : Type u) (β : Type v) (h : α →𝒄 β) :
α → β

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
theorem omega_complete_partial_order.continuous_hom.congr_fun {α : Type u} {β : Type v} {f g : α →𝒄 β} (h : f = g) (x : α) :
f x = g x
theorem omega_complete_partial_order.continuous_hom.congr_arg {α : Type u} {β : Type v} (f : α →𝒄 β) {x y : α} (h : x = y) :
f x = f y
@[protected]
theorem omega_complete_partial_order.continuous_hom.monotone {α : Type u} {β : Type v} (f : α →𝒄 β) :
theorem omega_complete_partial_order.continuous_hom.apply_mono {α : Type u} {β : Type v} {f g : α →𝒄 β} {x y : α} (h₁ : f g) (h₂ : x y) :
f x g y
theorem omega_complete_partial_order.continuous_hom.ite_continuous' {α : Type u} {β : Type v} {p : Prop} [hp : decidable p] (f g : α → β)  :
omega_complete_partial_order.continuous' (λ (x : α), ite p (f x) (g x))
theorem omega_complete_partial_order.continuous_hom.ωSup_bind {α : Type u} {β γ : Type v} (f : α →o part β) (g : α →o β → part γ) :
theorem omega_complete_partial_order.continuous_hom.bind_continuous' {α : Type u} {β γ : Type v} (f : α → part β) (g : α → β → part γ) :
theorem omega_complete_partial_order.continuous_hom.map_continuous' {α : Type u} {β γ : Type v} (f : β → γ) (g : α → part β)  :
theorem omega_complete_partial_order.continuous_hom.seq_continuous' {α : Type u} {β γ : Type v} (f : α → part (β → γ)) (g : α → part β)  :
theorem omega_complete_partial_order.continuous_hom.continuous {α : Type u} {β : Type v} (F : α →𝒄 β)  :
@[reducible]
def omega_complete_partial_order.continuous_hom.of_fun {α : Type u} {β : Type v} (f : α → β) (g : α →𝒄 β) (h : f = g) :
α →𝒄 β

Construct a continuous function from a bare function, a continuous function, and a proof that they are equal.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.of_fun_apply {α : Type u} {β : Type v} (f : α → β) (g : α →𝒄 β) (h : f = g) (ᾰ : α) :
= f ᾰ
@[reducible]
def omega_complete_partial_order.continuous_hom.of_mono {α : Type u} {β : Type v} (f : α →o β) (h : ∀ (c : , ) :
α →𝒄 β

Construct a continuous function from a monotone function with a proof of continuity.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.of_mono_apply {α : Type u} {β : Type v} (f : α →o β) (h : ∀ (c : , ) (ᾰ : α) :
@[simp]
theorem omega_complete_partial_order.continuous_hom.id_apply {α : Type u} (ᾰ : α) :

The identity as a continuous function.

Equations
def omega_complete_partial_order.continuous_hom.comp {α : Type u} {β : Type v} {γ : Type u_3} (f : β →𝒄 γ) (g : α →𝒄 β) :
α →𝒄 γ

The composition of continuous functions.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.comp_apply {α : Type u} {β : Type v} {γ : Type u_3} (f : β →𝒄 γ) (g : α →𝒄 β) (ᾰ : α) :
(f.comp g) = f (g ᾰ)
@[protected, ext]
theorem omega_complete_partial_order.continuous_hom.ext {α : Type u} {β : Type v} (f g : α →𝒄 β) (h : ∀ (x : α), f x = g x) :
f = g
@[protected]
theorem omega_complete_partial_order.continuous_hom.coe_inj {α : Type u} {β : Type v} (f g : α →𝒄 β) (h : f = g) :
f = g
@[simp]
theorem omega_complete_partial_order.continuous_hom.comp_id {β : Type v} {γ : Type u_3} (f : β →𝒄 γ) :
@[simp]
theorem omega_complete_partial_order.continuous_hom.id_comp {β : Type v} {γ : Type u_3} (f : β →𝒄 γ) :
@[simp]
theorem omega_complete_partial_order.continuous_hom.comp_assoc {α : Type u} {β : Type v} {γ : Type u_3} {φ : Type u_4} (f : γ →𝒄 φ) (g : β →𝒄 γ) (h : α →𝒄 β) :
f.comp (g.comp h) = (f.comp g).comp h
@[simp]
theorem omega_complete_partial_order.continuous_hom.coe_apply {α : Type u} {β : Type v} (a : α) (f : α →𝒄 β) :
f a = f a
def omega_complete_partial_order.continuous_hom.const {α : Type u} {β : Type v} (x : β) :
α →𝒄 β

function.const is a continuous function.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.const_apply {α : Type u} {β : Type v} (f : β) (a : α) :
@[protected, instance]
def omega_complete_partial_order.continuous_hom.inhabited {α : Type u} {β : Type v} [inhabited β] :
Equations
def omega_complete_partial_order.continuous_hom.to_mono {α : Type u} {β : Type v}  :
→𝒄 β) →o α →o β

The map from continuous functions to monotone functions is itself a monotone function.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.to_mono_coe {α : Type u} {β : Type v} (f : α →𝒄 β) :
@[simp]
theorem omega_complete_partial_order.continuous_hom.forall_forall_merge {α : Type u} {β : Type v} (c₀ : omega_complete_partial_order.chain →𝒄 β)) (z : β) :
(∀ (i j : ), (c₀ i) (c₁ j) z) ∀ (i : ), (c₀ i) (c₁ i) z

When proving that a chain of applications is below a bound z, it suffices to consider the functions and values being selected from the same index in the chains.

This lemma is more specific than necessary, i.e. c₀ only needs to be a chain of monotone functions, but it is only used with continuous functions.

@[simp]
theorem omega_complete_partial_order.continuous_hom.forall_forall_merge' {α : Type u} {β : Type v} (c₀ : omega_complete_partial_order.chain →𝒄 β)) (z : β) :
(∀ (j i : ), (c₀ i) (c₁ j) z) ∀ (i : ), (c₀ i) (c₁ i) z
@[protected]

The ωSup operator for continuous functions, which takes the pointwise countable supremum of the functions in the ω-chain.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.ωSup_apply {α : Type u} {β : Type v} (c : omega_complete_partial_order.chain →𝒄 β)) (ᾰ : α) :
@[simp]
@[protected, instance]
Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.prod.apply_apply {α : Type u} {β : Type v} (f : →𝒄 β) × α) :
def omega_complete_partial_order.continuous_hom.prod.apply {α : Type u} {β : Type v}  :
→𝒄 β) × α →𝒄 β

The application of continuous functions as a continuous function.

Equations
theorem omega_complete_partial_order.continuous_hom.ωSup_def {α : Type u} {β : Type v} (c : omega_complete_partial_order.chain →𝒄 β)) (x : α) :
@[simp]
theorem omega_complete_partial_order.continuous_hom.flip_apply {β : Type v} {γ : Type u_3} {α : Type u_1} (f : α → β →𝒄 γ) (x : β) (y : α) :
= (f y) x
def omega_complete_partial_order.continuous_hom.flip {β : Type v} {γ : Type u_3} {α : Type u_1} (f : α → β →𝒄 γ) :
β →𝒄 α → γ

A family of continuous functions yields a continuous family of functions.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.bind_apply {α : Type u} {β γ : Type v} (f : α →𝒄 part β) (g : α →𝒄 β → part γ) (ᾰ : α) :
(f.bind g) = (f.bind g)
noncomputable def omega_complete_partial_order.continuous_hom.bind {α : Type u} {β γ : Type v} (f : α →𝒄 part β) (g : α →𝒄 β → part γ) :

part.bind as a continuous function.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.map_apply {α : Type u} {β γ : Type v} (f : β → γ) (g : α →𝒄 part β) (x : α) :
= f <\$> g x
noncomputable def omega_complete_partial_order.continuous_hom.map {α : Type u} {β γ : Type v} (f : β → γ) (g : α →𝒄 part β) :

part.map as a continuous function.

Equations
noncomputable def omega_complete_partial_order.continuous_hom.seq {α : Type u} {β γ : Type v} (f : α →𝒄 part (β → γ)) (g : α →𝒄 part β) :

part.seq as a continuous function.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.seq_apply {α : Type u} {β γ : Type v} (f : α →𝒄 part (β → γ)) (g : α →𝒄 part β) (x : α) :
(f.seq g) x = f x <*> g x