Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-03 15:50 63d109fe

View on Github →

chore(category_theory/limits): Use lim_map over lim.map (#4856) Modify the simp-normal form for lim.map to be lim_map instead, and express lemmas in terms of lim_map instead, as well as use it in special shapes so that the assumptions can be weakened.

Estimated changes