mathlib3 documentation

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 #

Instances of omega_complete_partial_order #

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
@[protected, instance]
Equations

map function for chain

Equations
@[simp]
theorem omega_complete_partial_order.chain.map_coe {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) (f : α →o β) :
(c.map f) = f c
theorem omega_complete_partial_order.chain.mem_map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {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 β] (c : omega_complete_partial_order.chain α) {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 β] (c : omega_complete_partial_order.chain α) {f : α →o β} {b : β} :
b c.map f (a : α), a c f a = b
theorem omega_complete_partial_order.chain.map_comp {α : Type u} {β : Type v} {γ : Type u_1} [preorder α] [preorder β] [preorder γ] (c : omega_complete_partial_order.chain α) {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 β] (c : omega_complete_partial_order.chain α) {f g : α →o β} (h : f g) :
c.map f c.map g

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

Equations
@[simp]
theorem omega_complete_partial_order.chain.zip_coe {α : Type u} {β : Type v} [preorder α] [preorder β] (c₀ : omega_complete_partial_order.chain α) (c₁ : omega_complete_partial_order.chain β) (x : ) :
(c₀.zip c₁) x = (c₀ x, c₁ x)
@[class]
structure omega_complete_partial_order (α : Type u_1) :
Type u_1

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]

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

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

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

Equations
theorem part.eq_of_chain {α : Type u} {c : omega_complete_partial_order.chain (part α)} {a b : α} (ha : part.some a c) (hb : part.some b c) :
a = b
@[protected]
noncomputable def part.ωSup {α : Type u} (c : omega_complete_partial_order.chain (part α)) :
part α

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

Equations
theorem pi.omega_complete_partial_order.flip₁_continuous' {α : Type u_1} {β : α Type u_2} {γ : Type u_3} [Π (x : α), omega_complete_partial_order (β x)] [omega_complete_partial_order γ] (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 : α), omega_complete_partial_order (β x)] [omega_complete_partial_order γ] (f : γ Π (x : α), β x) (hf : (x : α), omega_complete_partial_order.continuous' (λ (g : γ), f g x)) :
@[protected]

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

Equations
@[protected, instance]

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

Equations
@[protected, instance]
Equations

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

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.apply_mono {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] {f g : α →𝒄 β} {x y : α} (h₁ : f g) (h₂ : x y) :
f x g y
@[reducible]

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

Equations
@[reducible]

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

Equations

The composition of continuous functions.

Equations
@[simp]
@[protected, ext]
theorem omega_complete_partial_order.continuous_hom.ext {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f g : α →𝒄 β) (h : (x : α), f x = g x) :
f = g

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

Equations
@[simp]

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.

The application of continuous functions as a continuous function.

Equations

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

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

part.bind as a continuous function.

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