Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-16 00:56 b0b61e6f

View on Github →

feat(order/category/omega-complete): omega-complete partial orders form a complete category (#4397) as discussed in #4348.

Estimated changes

Modified src/category_theory/limits/shapes/biproducts.lean

Modified src/category_theory/limits/shapes/equalizers.lean

deleted theorem category_theory.limits.cofork.of_π_app_one

deleted theorem category_theory.limits.cofork.of_π_app_zero

deleted theorem category_theory.limits.fork.of_ι_app_one

deleted theorem category_theory.limits.fork.of_ι_app_zero

Modified src/category_theory/limits/shapes/products.lean

modified def category_theory.limits.cofan.mk

deleted theorem category_theory.limits.cofan.mk_π_app

modified def category_theory.limits.fan.mk

deleted theorem category_theory.limits.fan.mk_π_app

Modified src/category_theory/limits/shapes/types.lean

Modified src/order/category/omega_complete_partial_order.lean

added def ωCPO.has_equalizers.equalizer

added def ωCPO.has_equalizers.equalizer_ι

added def ωCPO.has_equalizers.is_equalizer

added def ωCPO.has_products.is_product

added def ωCPO.has_products.product

modified def ωCPO

Modified src/order/omega_complete_partial_order.lean

added theorem omega_complete_partial_order.continuous_hom.congr_arg

added theorem omega_complete_partial_order.continuous_hom.congr_fun

added def omega_complete_partial_order.subtype

Modified src/order/preorder_hom.lean

added def preorder_hom.subtype.val