Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 16:37 6c2f80c9

View on Github →

feat(category_theory/limits): disjoint coproducts (#8380) Towards a more detailed hierarchy of categorical properties.

Estimated changes

Created src/category_theory/limits/shapes/disjoint_coproduct.lean

added theorem category_theory.limits.initial_mono_class_of_disjoint_coproducts

added def category_theory.limits.is_initial_of_is_pullback_of_is_coproduct