Commit 2023-06-29 08:26 d73ed56c

View on Github →

feat: port Order.Category.OmegaCompletePartialOrder (#5578)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/OmegaCompletePartialOrder.lean

added def ωCPO.HasEqualizers.equalizer

added def ωCPO.HasEqualizers.equalizerι

added def ωCPO.HasEqualizers.isEqualizer

added def ωCPO.HasProducts.isProduct

added def ωCPO.HasProducts.product

added theorem ωCPO.coe_of

added def ωCPO.of

added def ωCPO