mathlib documentation


Category of types with a omega complete partial order #

In this file, we bundle the class omega_complete_partial_order into a concrete category and prove that continuous functions also form a omega_complete_partial_order.

Main definitions #

def ωCPO.of (α : Type u_1) [omega_complete_partial_order α] :

Construct a bundled ωCPO from the underlying type and typeclass.

theorem ωCPO.coe_of (α : Type u_1) [omega_complete_partial_order α] :
(ωCPO.of α) = α
def ωCPO.has_products.product {J : Type v} (f : J → ωCPO) :

The pi-type gives a cone for a product.


The pi-type is a limit cone for the product.

def ωCPO.has_equalizers.equalizer_ι {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (f g : α →𝒄 β) :
{a // f a = g a} →𝒄 α

The equalizer inclusion function as a continuous_hom.