Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-02 17:36 62677179

View on Github →

fix(category_theory/limits): namespaces for is_(co)limit

Estimated changes

Modified category_theory/limits/cones.lean

Modified category_theory/limits/limits.lean

modified def category_theory.limits.is_colimit.desc_cocone_morphism

modified theorem category_theory.limits.is_colimit.hom_desc

modified theorem category_theory.limits.is_colimit.hom_ext

modified def category_theory.limits.is_colimit.hom_iso'

modified def category_theory.limits.is_colimit.hom_iso

modified theorem category_theory.limits.is_colimit.hom_iso_hom

modified def category_theory.limits.is_colimit.mk_cocone_morphism

modified def category_theory.limits.is_colimit.nat_iso

modified def category_theory.limits.is_colimit.of_iso_colimit

modified theorem category_theory.limits.is_colimit.uniq_cocone_morphism

modified def category_theory.limits.is_colimit.unique

modified theorem category_theory.limits.is_limit.hom_ext

modified def category_theory.limits.is_limit.hom_iso'

modified def category_theory.limits.is_limit.hom_iso

modified theorem category_theory.limits.is_limit.hom_iso_hom

modified theorem category_theory.limits.is_limit.hom_lift

modified def category_theory.limits.is_limit.lift_cone_morphism

modified def category_theory.limits.is_limit.mk_cone_morphism

modified def category_theory.limits.is_limit.nat_iso

modified def category_theory.limits.is_limit.of_iso_limit

modified theorem category_theory.limits.is_limit.uniq_cone_morphism

modified def category_theory.limits.is_limit.unique