Documentation

Mathlib.Order.Category.OmegaCompletePartialOrder

Category of types with an omega complete partial order #

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

Main definitions #

def ωCPO :
Type (u + 1)

The category of types with an omega complete partial order.

Equations
Instances For

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

    Equations
    Instances For
      @[simp]
      theorem ωCPO.coe_of (α : Type u_1) [OmegaCompletePartialOrder α] :
      (of α) = α

      The pi-type gives a cone for a product.

      Equations
      Instances For

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The equalizer inclusion function as a ContinuousHom.

          Equations
          Instances For

            The equalizer fork is a limit.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For