Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-05 07:50 3972da8a

View on Github →

chore(category_theory/limits/preserves): make names consistent (#5240) adjusted names and namespaces to match #5044

Estimated changes

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

added def category_theory.limits.is_limit_fan_mk_obj_of_is_limit

added def category_theory.limits.is_limit_map_cone_fan_mk_equiv

added def category_theory.limits.is_limit_of_has_product_of_preserves_limit

added def category_theory.limits.is_limit_of_is_limit_fan_mk_obj

added def category_theory.limits.preserves_product.iso

added theorem category_theory.limits.preserves_product.iso_hom

added def category_theory.limits.preserves_product.of_iso_comparison

deleted def preserves.fan_map_cone_limit

deleted def preserves.is_limit_of_has_product_of_preserves_limit

deleted def preserves.is_limit_of_reflects_of_map_is_limit

deleted def preserves.map_is_limit_of_preserves_of_is_limit

deleted def preserves.preserves_product_of_iso_comparison

deleted def preserves.preserves_products_iso

deleted theorem preserves.preserves_products_iso_hom

Modified src/topology/sheaves/forget.lean