Commit 2021-01-15 08:35 f8db86a2

View on Github →

feat(category_theory/limits): finite products from binary products (#5516) Adds constructions for finite products from binary products and terminal object, and a preserves version

Estimated changes

Created src/category_theory/limits/shapes/constructions/finite_products_of_binary_products.lean

added def category_theory.extend_fan

added def category_theory.extend_fan_is_limit

added theorem category_theory.has_finite_products_of_has_binary_and_terminal

added def category_theory.preserves_finite_products_of_preserves_binary_and_terminal

added def category_theory.preserves_ulift_fin_of_preserves_binary_and_terminal