Commit 2023-05-17 23:10 dd5ae6b3

View on Github →

feat: port CategoryTheory.Limits.Constructions.Over.Products (#4046)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

added def CategoryTheory.Over.ConstructProducts.conesEquiv

added def CategoryTheory.Over.ConstructProducts.conesEquivCounitIso

added def CategoryTheory.Over.ConstructProducts.conesEquivFunctor

added def CategoryTheory.Over.ConstructProducts.conesEquivInverse

added def CategoryTheory.Over.ConstructProducts.conesEquivInverseObj

added def CategoryTheory.Over.ConstructProducts.conesEquivUnitIso

added theorem CategoryTheory.Over.ConstructProducts.has_over_limit_discrete_of_widePullback_limit

added theorem CategoryTheory.Over.ConstructProducts.over_binaryProduct_of_pullback

added theorem CategoryTheory.Over.ConstructProducts.over_finiteProducts_of_finiteWidePullbacks

added theorem CategoryTheory.Over.ConstructProducts.over_product_of_widePullback

added theorem CategoryTheory.Over.ConstructProducts.over_products_of_widePullbacks

added def CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver

added theorem CategoryTheory.Over.over_hasTerminal