Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-03-07 14:11
9ed43666
View on Github →
feat(category_theory/limits): limit preservation properties of functor.left_op and similar (
#12168
)
Estimated changes
Created
src/category_theory/limits/preserves/opposites.lean
added
def
category_theory.limits.perserves_colimits_op
added
def
category_theory.limits.preserves_colimit_left_op
added
def
category_theory.limits.preserves_colimit_op
added
def
category_theory.limits.preserves_colimit_right_op
added
def
category_theory.limits.preserves_colimit_unop
added
def
category_theory.limits.preserves_colimits_left_op
added
def
category_theory.limits.preserves_colimits_of_shape_left_op
added
def
category_theory.limits.preserves_colimits_of_shape_op
added
def
category_theory.limits.preserves_colimits_of_shape_right_op
added
def
category_theory.limits.preserves_colimits_of_shape_unop
added
def
category_theory.limits.preserves_colimits_right_op
added
def
category_theory.limits.preserves_colimits_unop
added
def
category_theory.limits.preserves_finite_colimits_left_op
added
def
category_theory.limits.preserves_finite_colimits_op
added
def
category_theory.limits.preserves_finite_colimits_right_op
added
def
category_theory.limits.preserves_finite_colimits_unop
added
def
category_theory.limits.preserves_finite_limits_left_op
added
def
category_theory.limits.preserves_finite_limits_op
added
def
category_theory.limits.preserves_finite_limits_right_op
added
def
category_theory.limits.preserves_finite_limits_unop
added
def
category_theory.limits.preserves_limit_left_op
added
def
category_theory.limits.preserves_limit_op
added
def
category_theory.limits.preserves_limit_right_op
added
def
category_theory.limits.preserves_limit_unop
added
def
category_theory.limits.preserves_limits_left_op
added
def
category_theory.limits.preserves_limits_of_shape_left_op
added
def
category_theory.limits.preserves_limits_of_shape_op
added
def
category_theory.limits.preserves_limits_of_shape_right_op
added
def
category_theory.limits.preserves_limits_of_shape_unop
added
def
category_theory.limits.preserves_limits_op
added
def
category_theory.limits.preserves_limits_right_op
added
def
category_theory.limits.preserves_limits_unop