Commit 2019-06-18 22:06 235b8992
View on Github →fix(category_theory/types): rename lemma ulift_functor.map
(#1133)
- fix(category_theory/types): avoid shadowing
ulift_functor.map
by a lemma Now we can useulift_functor.map
in the sensefunctor.map ulift_functor
. ulift_functor.map_spec
→ulift_functor_map
as suggested by @semorrison in https://github.com/leanprover-community/mathlib/pull/1133#pullrequestreview-250179914