# mathlib3documentation

order.omega_complete_partial_order

# Omega Complete Partial Orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

A chain is a monotone sequence.

See the definition on page 114 of [Gun92].

Equations
Instances for `omega_complete_partial_order.chain`
@[protected, instance]
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 c f 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_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 y x 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_iff {α : Type u} (x : α) :
(i : ), c i x
def omega_complete_partial_order.subtype {α : Type u_1} (p : α Prop) (hp : (c : , ( (i : α), i c p 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 : α →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 : α), ] :
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]
@[simp]
@[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]

The `ωSup` operator for monotone functions.

Equations
@[simp]
@[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 β)  :
@[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]

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]
Equations

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

Equations
@[simp]
@[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]
@[simp]
@[protected, instance]
Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.prod.apply_apply {α : Type u} {β : Type v} (f : →𝒄 β) × α) :

The application of continuous functions as a continuous function.

Equations
@[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