Commit 2023-03-09 06:58 a7c8789d

View on Github →

feat: port CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (#2738)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

added def CategoryTheory.extendCofan

added def CategoryTheory.extendCofanIsColimit

added def CategoryTheory.extendFan

added def CategoryTheory.extendFanIsLimit

added theorem CategoryTheory.hasFiniteCoproducts_of_has_binary_and_initial

added theorem CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal

added def CategoryTheory.preservesFiniteCoproductsOfPreservesBinaryAndInitial

added def CategoryTheory.preservesFiniteProductsOfPreservesBinaryAndTerminal

added def CategoryTheory.preservesShapeFinOfPreservesBinaryAndInitial

added def CategoryTheory.preservesShapeFinOfPreservesBinaryAndTerminal