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.