Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-21 21:06 a6078202

View on Github →

feat(category_theory/equivalence): if two functors F and G are isomorphic, F is an equivalence iff G is (#12162)

Estimated changes

Modified src/category_theory/equivalence.lean

added def category_theory.is_equivalence.cancel_comp_left

added def category_theory.is_equivalence.cancel_comp_right

added def category_theory.is_equivalence.equiv_of_iso

added def category_theory.is_equivalence.of_iso

added theorem category_theory.is_equivalence.of_iso_refl

added theorem category_theory.is_equivalence.of_iso_trans