mathlib

b0b61e6f - feat(order/category/omega-complete): omega-complete partial orders form a complete category (#4397)

feat(order/category/omega-complete): omega-complete partial orders form a complete category (#4397) as discussed in #4348. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>