Commit 2023-03-13 13:46 73599160

View on Github →

feat: port CategoryTheory.Limits.ColimitLimit (#2810)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/ColimitLimit.lean

added theorem CategoryTheory.Limits.map_id_left_eq_curry_map

added theorem CategoryTheory.Limits.map_id_right_eq_curry_swap_map

added theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π

added theorem CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply