Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-03 15:11 97265f9c

View on Github →

feat(category_theory/limits): dualise a limits result (#2940) Add the dual of is_limit.of_cone_equiv.

Estimated changes

Modified src/category_theory/adjunction/basic.lean

added def category_theory.adjunction.of_left_adjoint

added def category_theory.adjunction.of_right_adjoint

Modified src/category_theory/limits/cones.lean

Modified src/category_theory/limits/limits.lean

added def category_theory.limits.is_colimit.of_cocone_equiv

modified def category_theory.limits.is_limit.of_cone_equiv

Modified src/category_theory/limits/over.lean

Modified src/category_theory/limits/preserves.lean

added def category_theory.limits.preserves_colimit_of_iso