Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-06 07:44 b4d007fc

View on Github →

feat(category_theory/limits): transport is_limit along F.left_op and similar (#12166)

Estimated changes

Modified src/category_theory/limits/opposites.lean

modified theorem category_theory.limits.has_colimit_of_has_limit_left_op

modified theorem category_theory.limits.has_limit_of_has_colimit_left_op

added def category_theory.limits.is_colimit_cocone_left_op_of_cone

added def category_theory.limits.is_colimit_cocone_of_cone_left_op

added def category_theory.limits.is_colimit_cocone_of_cone_right_op

added def category_theory.limits.is_colimit_cocone_right_op_of_cone

added def category_theory.limits.is_colimit_cocone_unop_of_cone

added def category_theory.limits.is_colimit_cone_of_cocone_unop

added def category_theory.limits.is_colimit_cone_op

added def category_theory.limits.is_colimit_cone_unop

added def category_theory.limits.is_limit_cocone_op

added def category_theory.limits.is_limit_cocone_unop

added def category_theory.limits.is_limit_cone_left_op_of_cocone

added def category_theory.limits.is_limit_cone_of_cocone_left_op

added def category_theory.limits.is_limit_cone_of_cocone_right_op

added def category_theory.limits.is_limit_cone_of_cocone_unop

added def category_theory.limits.is_limit_cone_right_op_of_cocone

added def category_theory.limits.is_limit_cone_unop_of_cocone