Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-02 11:46 fe4da7bc

View on Github →

feat(category_theory/limits): transporting is_limit (#3598) Some lemmas about moving is_limit terms around over equivalences, or (post|pre)composing.

Estimated changes

Modified src/category_theory/limits/limits.lean

added def category_theory.limits.is_colimit.hom_is_iso

added def category_theory.limits.is_colimit.of_left_adjoint

added def category_theory.limits.is_colimit.precompose_hom_equiv

added def category_theory.limits.is_colimit.precompose_inv_equiv

added def category_theory.limits.is_limit.hom_is_iso

added def category_theory.limits.is_limit.of_right_adjoint

added def category_theory.limits.is_limit.postcompose_hom_equiv

added def category_theory.limits.is_limit.postcompose_inv_equiv

Modified src/category_theory/limits/preserves.lean

Modified src/category_theory/limits/shapes/constructions/over/products.lean