Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 03:09 cb45da26

View on Github →

feat(category_theory/limits): is_bilimit (#12108)

Estimated changes

Modified src/category_theory/limits/shapes/biproducts.lean

added structure category_theory.limits.bicone.is_bilimit

added def category_theory.limits.bicone.of_colimit_cocone

added def category_theory.limits.bicone.of_limit_cone

added def category_theory.limits.bicone.to_binary_bicone_is_bilimit

modified def category_theory.limits.bicone.to_binary_bicone_is_colimit

modified def category_theory.limits.bicone.to_binary_bicone_is_limit

added theorem category_theory.limits.bicone.ι_of_is_limit

added theorem category_theory.limits.bicone.π_of_is_colimit

modified theorem category_theory.limits.bicone_ι_π_ne

added structure category_theory.limits.binary_bicone.is_bilimit

added def category_theory.limits.binary_bicone.to_bicone

added def category_theory.limits.binary_bicone.to_bicone_is_bilimit

added def category_theory.limits.binary_bicone.to_bicone_is_colimit

added def category_theory.limits.binary_bicone.to_bicone_is_limit

added def category_theory.limits.binary_biproduct.is_bilimit

added def category_theory.limits.biproduct.is_bilimit