Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-28 04:36 b02bea6e

View on Github →

feat(category_theory/equivalence): equivalences, slice tactic (#479)

Estimated changes

Modified category_theory/category.lean

Created category_theory/equivalence.lean

added def category_theory.category_theory.equivalence.equivalence_of_fully_faithfully_ess_surj

added def category_theory.category_theory.equivalence.ess_surj_of_equivalence

added theorem category_theory.equivalence.fun_inv_map

added theorem category_theory.equivalence.inv_fun_map

added def category_theory.equivalence.refl

added def category_theory.equivalence.symm

added def category_theory.equivalence.trans

added structure category_theory.equivalence

added def category_theory.functor.as_equivalence

added def category_theory.functor.fun_inv_id

added def category_theory.functor.fun_obj_preimage_iso

added def category_theory.functor.inv

added def category_theory.functor.inv_fun_id

added def category_theory.functor.obj_preimage

added theorem category_theory.is_equivalence.fun_inv_map

added theorem category_theory.is_equivalence.inv_fun_map

Modified category_theory/natural_isomorphism.lean

added theorem category_theory.nat_iso.hom_app_inv_app_id

added theorem category_theory.nat_iso.hom_vcomp_inv

added theorem category_theory.nat_iso.inv_app_hom_app_id

added theorem category_theory.nat_iso.inv_vcomp_hom

Created tactic/slice.lean