Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-11 04:03 ef46da81

View on Github →

feat(category_theory/*): Curried yoneda lemma (#9579) Provided curried versions of the Yoneda lemma when the category is small.

Estimated changes

Modified src/category_theory/closed/cartesian.lean

added theorem category_theory.cartesian_closed.curry_eq

added theorem category_theory.cartesian_closed.curry_eq_iff

added theorem category_theory.cartesian_closed.curry_id_eq_coev

added theorem category_theory.cartesian_closed.curry_injective

added theorem category_theory.cartesian_closed.curry_natural_left

added theorem category_theory.cartesian_closed.curry_natural_right

added theorem category_theory.cartesian_closed.curry_uncurry

added theorem category_theory.cartesian_closed.eq_curry_iff

added theorem category_theory.cartesian_closed.uncurry_curry

added theorem category_theory.cartesian_closed.uncurry_eq

added theorem category_theory.cartesian_closed.uncurry_id_eq_ev

added theorem category_theory.cartesian_closed.uncurry_injective

added theorem category_theory.cartesian_closed.uncurry_natural_left

added theorem category_theory.cartesian_closed.uncurry_natural_right

deleted theorem category_theory.curry_eq

deleted theorem category_theory.curry_eq_iff

deleted theorem category_theory.curry_id_eq_coev

deleted theorem category_theory.curry_injective

deleted theorem category_theory.curry_natural_left

deleted theorem category_theory.curry_natural_right

deleted theorem category_theory.curry_uncurry

deleted theorem category_theory.eq_curry_iff

deleted theorem category_theory.uncurry_curry

deleted theorem category_theory.uncurry_eq

deleted theorem category_theory.uncurry_id_eq_ev

deleted theorem category_theory.uncurry_injective

deleted theorem category_theory.uncurry_natural_left

deleted theorem category_theory.uncurry_natural_right

Modified src/category_theory/closed/functor.lean

Modified src/category_theory/closed/ideal.lean

Modified src/category_theory/types.lean

added def category_theory.ulift_functor_trivial

Modified src/category_theory/yoneda.lean

added def category_theory.curried_yoneda_lemma'

added def category_theory.curried_yoneda_lemma