Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.equivalence.to_order_iso_apply

Modification history

2021-09-04 06:46

src/category_theory/category/preorder.lean

feat(category_theory/basic/category): Combine and improve API on preorder categories. (#8982) …

Modified category_theory.equivalence.to_order_iso_apply View on Github →

2021-04-06 09:41

src/category_theory/equivalence.lean

feat(category_theory): Type u is well-powered (#6812) …

Added category_theory.equivalence.to_order_iso_apply View on Github →