Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-20 10:08 4db82a40

View on Github →

refactor(category_theory/cones): golf and cleanup cones (#6756) No mathematical content here, basically just golfing and tidying in preparation for future PRs.

Estimated changes

Modified src/category_theory/limits/cones.lean

modified def category_theory.functor.cones

modified def category_theory.limits.cocone.extend

deleted theorem category_theory.limits.cocone.extend_ι

modified def category_theory.limits.cocone.extensions

modified def category_theory.limits.cocone.whisker

modified def category_theory.limits.cocones.equivalence_of_reindexing

modified def category_theory.limits.cocones.whiskering

modified def category_theory.limits.cocones.whiskering_equivalence

modified def category_theory.limits.cone.extend

deleted theorem category_theory.limits.cone.extend_π

modified def category_theory.limits.cone.extensions

modified def category_theory.limits.cone.whisker

modified def category_theory.limits.cones.equivalence_of_reindexing

modified def category_theory.limits.cones.whiskering

modified def category_theory.limits.cones.whiskering_equivalence

Modified src/category_theory/limits/is_limit.lean