Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-08 07:36 73601789

View on Github →

feat(category_theory/closed/types): presheaf category is cartesian closed (#4897)

Estimated changes

Created src/category_theory/closed/types.lean

Modified src/category_theory/limits/preserves/limits.lean

added theorem category_theory.lift_comp_preserves_limits_iso_hom

added def category_theory.preserves_colimit_iso

added theorem category_theory.preserves_colimits_iso_inv_comp_desc

added theorem category_theory.preserves_desc_map_cocone

added theorem category_theory.preserves_lift_map_cone

added def category_theory.preserves_limit_iso

added theorem category_theory.preserves_limits_iso_hom_π

added theorem category_theory.preserves_limits_iso_inv_π

added theorem category_theory.ι_preserves_colimits_iso_hom

added theorem category_theory.ι_preserves_colimits_iso_inv

deleted theorem lift_comp_preserves_limits_iso_hom

deleted def preserves_colimit_iso

deleted theorem preserves_colimits_iso_inv_comp_desc

deleted theorem preserves_desc_map_cocone

deleted theorem preserves_lift_map_cone

deleted def preserves_limit_iso

deleted theorem preserves_limits_iso_hom_π

deleted theorem preserves_limits_iso_inv_π

deleted theorem ι_preserves_colimits_iso_hom

deleted theorem ι_preserves_colimits_iso_inv