FinPartialOrder): The category of finite partial orders (#11997)

Commit

4 years ago

feat(order/category/FinPartialOrder): The category of finite partial orders (#11997) Define `FinPartialOrder`, the category of finite partial orders with monotone functions.

Author

YaelDillies

Parents

56115334

mathlib fa603fed - feat(order/category/FinPartialOrder): The category of finite partial orders (#11997)

mathlib
fa603fed - feat(order/category/FinPartialOrder): The category of finite partial orders (#11997)