Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-16 01:06 a991854f

View on Github →

feat(category_theory/limits): a Fubini theorem (#3732)

Estimated changes

Modified src/category_theory/currying.lean

Created src/category_theory/limits/fubini.lean

added def category_theory.limits.cone_of_cone_uncurry

added def category_theory.limits.cone_of_cone_uncurry_is_limit

added def category_theory.limits.diagram_of_cones.cone_points

added def category_theory.limits.diagram_of_cones.mk_of_has_limits

added theorem category_theory.limits.diagram_of_cones.mk_of_has_limits_cone_points

added structure category_theory.limits.diagram_of_cones

added def category_theory.limits.limit_iso_limit_curry_comp_lim

added theorem category_theory.limits.limit_iso_limit_curry_comp_lim_hom_π_π

added theorem category_theory.limits.limit_iso_limit_curry_comp_lim_inv_π

added def category_theory.limits.limit_uncurry_iso_limit_comp_lim

added theorem category_theory.limits.limit_uncurry_iso_limit_comp_lim_hom_π_π

added theorem category_theory.limits.limit_uncurry_iso_limit_comp_lim_inv_π

Modified src/category_theory/limits/limits.lean