mathlib3 documentation


Category of types with a omega complete partial order #

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

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 #

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

theorem ωCPO.coe_of (α : Type u_1) [omega_complete_partial_order α] :
(ωCPO.of α) = α

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.