Mathlib Changelog
v3
Changelog
About
Github
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