PiProd

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean

Statistics

Metric	Count
Definitions binaryFanOfProp, binaryFanOfPropIsLimit	2
Theorems map_eq_prod_map, hasBinaryProduct_of_products	2
Total	4

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasBinaryProduct_of_products 📖	mathematical	—	HasBinaryProduct piObj	—	—

CategoryTheory.Limits.Pi

Definitions

Name	Category	Theorems
binaryFanOfProp 📖	CompOp	1 math math: map_eq_prod_map
binaryFanOfPropIsLimit 📖	CompOp	1 math math: map_eq_prod_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_eq_prod_map 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.piObj binaryFanOfProp CategoryTheory.Limits.prod CategoryTheory.Limits.hasBinaryProduct_of_products CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd CategoryTheory.Iso.hom CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso binaryFanOfPropIsLimit CategoryTheory.Limits.prodIsProd CategoryTheory.Limits.prod.map CategoryTheory.Iso.inv	—	CategoryTheory.Limits.hasBinaryProduct_of_products CategoryTheory.Category.assoc CategoryTheory.Iso.eq_comp_inv CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.prod.lift_map CategoryTheory.Limits.prod.hom_ext hom_ext CategoryTheory.Limits.limit.lift_π map'_comp_π map_π map'_comp_π_assoc CategoryTheory.Category.id_comp

---

← Back to Index