Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 08:57 0453320a

View on Github →

feat(category_theory/limits): The product is the pullback over the terminal objects. (#10581)

Estimated changes

Modified src/category_theory/limits/constructions/binary_products.lean

added theorem has_binary_coproducts_of_initial_and_pushouts

added def is_coproduct_of_is_initial_is_pushout

added def is_product_of_is_terminal_is_pullback

added def is_pullback_of_is_terminal_is_product

added def is_pushout_of_is_initial_is_coproduct