Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-15 05:11 51a75ffe

View on Github →

feat(category_theory/pullback): make the is_limit helper lemmas more ergonomic (#3398)

Estimated changes

Modified src/category_theory/abelian/non_preadditive.lean

Modified src/category_theory/limits/shapes/constructions/pullbacks.lean

Modified src/category_theory/limits/shapes/pullbacks.lean

deleted def category_theory.limits.pullback_cone.is_limit.mk'

modified def category_theory.limits.pullback_cone.is_limit.mk

added def category_theory.limits.pullback_cone.is_limit_aux'

added def category_theory.limits.pullback_cone.is_limit_aux

deleted def category_theory.limits.pushout_cocone.is_colimit.mk'

modified def category_theory.limits.pushout_cocone.is_colimit.mk

added def category_theory.limits.pushout_cocone.is_colimit_aux'

added def category_theory.limits.pushout_cocone.is_colimit_aux