Fubini

📁 Source: Mathlib/CategoryTheory/Limits/Fubini.lean

Statistics

Metric	Count
Definitions DiagramOfCocones, coconePoints, map, mkOfHasColimits, obj, DiagramOfCones, conePoints, map, mkOfHasLimits, obj, ofCoconeUncurry, ofConeOfConeUncurry, coconeOfCoconeCurry, coconeOfCoconeUncurry, coconeOfCoconeUncurryIsColimit, coconeOfHasColimitCurryCompColim, colimitCurrySwapCompColimIsoColimitCurryCompColim, colimitFlipCompColimIsoColimitCompColim, colimitIsoColimitCurryCompColim, colimitUncurryIsoColimitCompColim, coneOfConeCurry, coneOfConeUncurry, coneOfConeUncurryIsLimit, coneOfHasLimitCurryCompLim, diagramOfCoconesInhabited, diagramOfConesInhabited, isColimitCoconeOfHasColimitCurryCompColim, isLimitConeOfHasLimitCurryCompLim, limitCurrySwapCompLimIsoLimitCurryCompLim, limitFlipCompLimIsoLimitCompLim, limitIsoLimitCurryCompLim, limitUncurryIsoLimitCompLim	32
Theorems coconePoints_map, coconePoints_obj, comp, id, mkOfHasColimits_coconePoints, mkOfHasColimits_map_hom, mkOfHasColimits_obj, comp, conePoints_map, conePoints_obj, id, mkOfHasLimits_conePoints, mkOfHasLimits_map_hom, mkOfHasLimits_obj, coconeOfCoconeCurry_pt, coconeOfCoconeCurry_ι_app, coconeOfCoconeUncurry_pt, coconeOfCoconeUncurry_ι_app, colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom, colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv, colimitFlipCompColimIsoColimitCompColim_ι_ι_hom, colimitFlipCompColimIsoColimitCompColim_ι_ι_hom_assoc, colimitFlipCompColimIsoColimitCompColim_ι_ι_inv, colimitFlipCompColimIsoColimitCompColim_ι_ι_inv_assoc, colimitIsoColimitCurryCompColim_ι_hom, colimitIsoColimitCurryCompColim_ι_hom_assoc, colimitIsoColimitCurryCompColim_ι_ι_inv, colimitIsoColimitCurryCompColim_ι_ι_inv_assoc, colimitUncurryIsoColimitCompColim_ι_hom, colimitUncurryIsoColimitCompColim_ι_hom_assoc, colimitUncurryIsoColimitCompColim_ι_ι_inv, colimitUncurryIsoColimitCompColim_ι_ι_inv_assoc, coneOfConeCurry_pt, coneOfConeCurry_π_app, coneOfConeUncurry_pt, coneOfConeUncurry_π_app, instHasColimitProd, instHasLimitProd, limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π, limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π, limitFlipCompLimIsoLimitCompLim_hom_π_π, limitFlipCompLimIsoLimitCompLim_hom_π_π_assoc, limitFlipCompLimIsoLimitCompLim_inv_π_π, limitFlipCompLimIsoLimitCompLim_inv_π_π_assoc, limitIsoLimitCurryCompLim_hom_π_π, limitIsoLimitCurryCompLim_hom_π_π_assoc, limitIsoLimitCurryCompLim_inv_π, limitIsoLimitCurryCompLim_inv_π_assoc, limitUncurryIsoLimitCompLim_hom_π_π, limitUncurryIsoLimitCompLim_hom_π_π_assoc, limitUncurryIsoLimitCompLim_inv_π, limitUncurryIsoLimitCompLim_inv_π_assoc	52
Total	84

CategoryTheory.Limits

Definitions

Name	Category	Theorems
DiagramOfCocones 📖	CompData	—
DiagramOfCones 📖	CompData	—
coconeOfCoconeCurry 📖	CompOp	2 math math: coconeOfCoconeCurry_pt, coconeOfCoconeCurry_ι_app
coconeOfCoconeUncurry 📖	CompOp	2 math math: coconeOfCoconeUncurry_pt, coconeOfCoconeUncurry_ι_app
coconeOfCoconeUncurryIsColimit 📖	CompOp	—
coconeOfHasColimitCurryCompColim 📖	CompOp	—
colimitCurrySwapCompColimIsoColimitCurryCompColim 📖	CompOp	2 math math: colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom, colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv
colimitFlipCompColimIsoColimitCompColim 📖	CompOp	4 math math: colimitFlipCompColimIsoColimitCompColim_ι_ι_inv_assoc, colimitFlipCompColimIsoColimitCompColim_ι_ι_hom_assoc, colimitFlipCompColimIsoColimitCompColim_ι_ι_inv, colimitFlipCompColimIsoColimitCompColim_ι_ι_hom
colimitIsoColimitCurryCompColim 📖	CompOp	4 math math: colimitIsoColimitCurryCompColim_ι_hom_assoc, colimitIsoColimitCurryCompColim_ι_hom, colimitIsoColimitCurryCompColim_ι_ι_inv_assoc, colimitIsoColimitCurryCompColim_ι_ι_inv
colimitUncurryIsoColimitCompColim 📖	CompOp	4 math math: colimitUncurryIsoColimitCompColim_ι_ι_inv, colimitUncurryIsoColimitCompColim_ι_hom_assoc, colimitUncurryIsoColimitCompColim_ι_hom, colimitUncurryIsoColimitCompColim_ι_ι_inv_assoc
coneOfConeCurry 📖	CompOp	2 math math: coneOfConeCurry_pt, coneOfConeCurry_π_app
coneOfConeUncurry 📖	CompOp	2 math math: coneOfConeUncurry_π_app, coneOfConeUncurry_pt
coneOfConeUncurryIsLimit 📖	CompOp	—
coneOfHasLimitCurryCompLim 📖	CompOp	—
diagramOfCoconesInhabited 📖	CompOp	—
diagramOfConesInhabited 📖	CompOp	—
isColimitCoconeOfHasColimitCurryCompColim 📖	CompOp	—
isLimitConeOfHasLimitCurryCompLim 📖	CompOp	—
limitCurrySwapCompLimIsoLimitCurryCompLim 📖	CompOp	2 math math: limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π, limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π
limitFlipCompLimIsoLimitCompLim 📖	CompOp	4 math math: limitFlipCompLimIsoLimitCompLim_hom_π_π, limitFlipCompLimIsoLimitCompLim_inv_π_π, limitFlipCompLimIsoLimitCompLim_hom_π_π_assoc, limitFlipCompLimIsoLimitCompLim_inv_π_π_assoc
limitIsoLimitCurryCompLim 📖	CompOp	4 math math: limitIsoLimitCurryCompLim_hom_π_π_assoc, limitIsoLimitCurryCompLim_inv_π, limitIsoLimitCurryCompLim_inv_π_assoc, limitIsoLimitCurryCompLim_hom_π_π
limitUncurryIsoLimitCompLim 📖	CompOp	4 math math: limitUncurryIsoLimitCompLim_inv_π, limitUncurryIsoLimitCompLim_hom_π_π_assoc, limitUncurryIsoLimitCompLim_hom_π_π, limitUncurryIsoLimitCompLim_inv_π_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeOfCoconeCurry_pt 📖	mathematical	—	Cocone.pt DiagramOfCocones.coconePoints CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.Functor.category CategoryTheory.Functor.curry coconeOfCoconeCurry	—	—
coconeOfCoconeCurry_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app DiagramOfCocones.coconePoints CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.Functor.category CategoryTheory.Functor.curry CategoryTheory.Functor.const Cocone.pt Cocone.ι coconeOfCoconeCurry IsColimit.desc DiagramOfCocones.obj	—	—
coconeOfCoconeUncurry_pt 📖	mathematical	—	Cocone.pt DiagramOfCocones.coconePoints coconeOfCoconeUncurry CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry	—	—
coconeOfCoconeUncurry_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app DiagramOfCocones.coconePoints CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.pt CategoryTheory.prod' CategoryTheory.Functor.uncurry Cocone.ι coconeOfCoconeUncurry IsColimit.desc DiagramOfCocones.obj	—	—
colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.prod' CategoryTheory.Functor.curry CategoryTheory.Functor.comp CategoryTheory.Prod.swap colimit hasColimitOfHasColimitsOfShape colim colimit.ι CategoryTheory.Iso.hom colimitCurrySwapCompColimIsoColimitCurryCompColim	—	hasColimitOfHasColimitsOfShape instHasColimitProd CategoryTheory.Category.assoc colimitIsoColimitCurryCompColim_ι_ι_inv HasColimit.isoOfEquivalence_hom_π CategoryTheory.Category.id_comp colimit.w colimitIsoColimitCurryCompColim_ι_hom
colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.prod' CategoryTheory.Functor.curry colimit hasColimitOfHasColimitsOfShape CategoryTheory.Functor.comp CategoryTheory.Prod.swap colim colimit.ι CategoryTheory.Iso.inv colimitCurrySwapCompColimIsoColimitCurryCompColim	—	hasColimitOfHasColimitsOfShape instHasColimitProd CategoryTheory.Category.assoc colimitIsoColimitCurryCompColim_ι_ι_inv HasColimit.isoOfEquivalence_inv_π CategoryTheory.Bifunctor.map_id CategoryTheory.Category.id_comp colimitIsoColimitCurryCompColim_ι_hom
colimitFlipCompColimIsoColimitCompColim_ι_ι_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip colimit hasColimitOfHasColimitsOfShape CategoryTheory.Functor.comp colim colimit.ι CategoryTheory.Iso.hom colimitFlipCompColimIsoColimitCompColim	—	hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc colimitUncurryIsoColimitCompColim_ι_ι_inv HasColimit.isoOfNatIso_ι_hom CategoryTheory.Category.id_comp HasColimit.isoOfEquivalence_hom_π CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id colimitUncurryIsoColimitCompColim_ι_hom
colimitFlipCompColimIsoColimitCompColim_ι_ι_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip colimit hasColimitOfHasColimitsOfShape colimit.ι CategoryTheory.Functor.comp colim CategoryTheory.Iso.hom colimitFlipCompColimIsoColimitCompColim	—	hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimitFlipCompColimIsoColimitCompColim_ι_ι_hom
colimitFlipCompColimIsoColimitCompColim_ι_ι_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category colimit hasColimitOfHasColimitsOfShape CategoryTheory.Functor.comp CategoryTheory.Functor.flip colim colimit.ι CategoryTheory.Iso.inv colimitFlipCompColimIsoColimitCompColim	—	hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc colimitUncurryIsoColimitCompColim_ι_ι_inv HasColimit.isoOfEquivalence_inv_π CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp HasColimit.isoOfNatIso_ι_inv colimitUncurryIsoColimitCompColim_ι_hom
colimitFlipCompColimIsoColimitCompColim_ι_ι_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category colimit hasColimitOfHasColimitsOfShape colimit.ι CategoryTheory.Functor.comp colim CategoryTheory.Functor.flip CategoryTheory.Iso.inv colimitFlipCompColimIsoColimitCompColim	—	hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimitFlipCompColimIsoColimitCompColim_ι_ι_inv
colimitIsoColimitCurryCompColim_ι_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' colimit instHasColimitProd CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.curry colim colimit.ι CategoryTheory.Iso.hom colimitIsoColimitCurryCompColim hasColimitOfHasColimitsOfShape	—	instHasColimitProd hasColimitOfHasColimitsOfShape CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id colimitIsoColimitCurryCompColim_ι_ι_inv
colimitIsoColimitCurryCompColim_ι_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' colimit instHasColimitProd colimit.ι CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.curry colim CategoryTheory.Iso.hom colimitIsoColimitCurryCompColim hasColimitOfHasColimitsOfShape	—	instHasColimitProd hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimitIsoColimitCurryCompColim_ι_hom
colimitIsoColimitCurryCompColim_ι_ι_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.prod' CategoryTheory.Functor.curry colimit hasColimitOfHasColimitsOfShape instHasColimitProd colimit.ι CategoryTheory.Functor.comp colim CategoryTheory.Iso.inv colimitIsoColimitCurryCompColim	—	instHasColimitProd hasColimitOfHasColimitsOfShape colimit.comp_coconePointUniqueUpToIso_inv_assoc colimit.ι_desc_assoc HasColimit.isoOfNatIso_ι_inv CategoryTheory.Category.id_comp
colimitIsoColimitCurryCompColim_ι_ι_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.prod' CategoryTheory.Functor.curry colimit hasColimitOfHasColimitsOfShape colimit.ι CategoryTheory.Functor.comp colim instHasColimitProd CategoryTheory.Iso.inv colimitIsoColimitCurryCompColim	—	instHasColimitProd hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimitIsoColimitCurryCompColim_ι_ι_inv
colimitUncurryIsoColimitCompColim_ι_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry colimit CategoryTheory.Functor.comp colim colimit.ι CategoryTheory.Iso.hom colimitUncurryIsoColimitCompColim hasColimitOfHasColimitsOfShape	—	hasColimitOfHasColimitsOfShape CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id colimitUncurryIsoColimitCompColim_ι_ι_inv
colimitUncurryIsoColimitCompColim_ι_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry colimit colimit.ι CategoryTheory.Functor.comp colim CategoryTheory.Iso.hom colimitUncurryIsoColimitCompColim hasColimitOfHasColimitsOfShape	—	hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimitUncurryIsoColimitCompColim_ι_hom
colimitUncurryIsoColimitCompColim_ι_ι_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category colimit hasColimitOfHasColimitsOfShape CategoryTheory.prod' CategoryTheory.Functor.uncurry colimit.ι CategoryTheory.Functor.comp colim CategoryTheory.Iso.inv colimitUncurryIsoColimitCompColim	—	hasColimitOfHasColimitsOfShape colimit.ι_desc
colimitUncurryIsoColimitCompColim_ι_ι_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category colimit hasColimitOfHasColimitsOfShape colimit.ι CategoryTheory.Functor.comp colim CategoryTheory.prod' CategoryTheory.Functor.uncurry CategoryTheory.Iso.inv colimitUncurryIsoColimitCompColim	—	hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimitUncurryIsoColimitCompColim_ι_ι_inv
coneOfConeCurry_pt 📖	mathematical	—	Cone.pt DiagramOfCones.conePoints CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.Functor.category CategoryTheory.Functor.curry coneOfConeCurry	—	—
coneOfConeCurry_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cone.pt CategoryTheory.prod' DiagramOfCones.conePoints CategoryTheory.Functor.curry Cone.π coneOfConeCurry IsLimit.lift DiagramOfCones.obj	—	—
coneOfConeUncurry_pt 📖	mathematical	—	Cone.pt DiagramOfCones.conePoints coneOfConeUncurry CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry	—	—
coneOfConeUncurry_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cone.pt CategoryTheory.prod' CategoryTheory.Functor.uncurry DiagramOfCones.conePoints Cone.π coneOfConeUncurry IsLimit.lift DiagramOfCones.obj	—	—
instHasColimitProd 📖	mathematical	—	HasColimit CategoryTheory.prod'	—	—
instHasLimitProd 📖	mathematical	—	HasLimit CategoryTheory.prod'	—	—
limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor.curry CategoryTheory.Prod.swap lim hasLimitOfHasLimitsOfShape CategoryTheory.Iso.hom limitCurrySwapCompLimIsoLimitCurryCompLim limit.π	—	hasLimitOfHasLimitsOfShape instHasLimitProd CategoryTheory.Category.assoc limitIsoLimitCurryCompLim_hom_π_π HasLimit.isoOfEquivalence_hom_π CategoryTheory.prod_id CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id limitIsoLimitCurryCompLim_inv_π
limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor.curry lim CategoryTheory.Prod.swap hasLimitOfHasLimitsOfShape CategoryTheory.Iso.inv limitCurrySwapCompLimIsoLimitCurryCompLim limit.π	—	hasLimitOfHasLimitsOfShape instHasLimitProd CategoryTheory.Iso.trans_assoc CategoryTheory.Category.assoc limitIsoLimitCurryCompLim_hom_π_π HasLimit.isoOfEquivalence_inv_π CategoryTheory.Category.comp_id limitIsoLimitCurryCompLim_inv_π
limitFlipCompLimIsoLimitCompLim_hom_π_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip lim hasLimitOfHasLimitsOfShape CategoryTheory.Functor.obj CategoryTheory.Iso.hom limitFlipCompLimIsoLimitCompLim limit.π	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc limitUncurryIsoLimitCompLim_hom_π_π HasLimit.isoOfEquivalence_hom_π CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id HasLimit.isoOfNatIso_hom_π limitUncurryIsoLimitCompLim_inv_π
limitFlipCompLimIsoLimitCompLim_hom_π_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip lim hasLimitOfHasLimitsOfShape CategoryTheory.Iso.hom limitFlipCompLimIsoLimitCompLim CategoryTheory.Functor.obj limit.π	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitFlipCompLimIsoLimitCompLim_hom_π_π
limitFlipCompLimIsoLimitCompLim_inv_π_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category lim hasLimitOfHasLimitsOfShape CategoryTheory.Functor.flip CategoryTheory.Functor.obj CategoryTheory.Iso.inv limitFlipCompLimIsoLimitCompLim limit.π	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc limitUncurryIsoLimitCompLim_hom_π_π HasLimit.isoOfNatIso_inv_π CategoryTheory.Category.comp_id HasLimit.isoOfEquivalence_inv_π limitUncurryIsoLimitCompLim_inv_π
limitFlipCompLimIsoLimitCompLim_inv_π_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category lim hasLimitOfHasLimitsOfShape CategoryTheory.Functor.flip CategoryTheory.Iso.inv limitFlipCompLimIsoLimitCompLim CategoryTheory.Functor.obj limit.π	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitFlipCompLimIsoLimitCompLim_inv_π_π
limitIsoLimitCurryCompLim_hom_π_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.prod' instHasLimitProd CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.curry lim CategoryTheory.Iso.hom limitIsoLimitCurryCompLim limit.π hasLimitOfHasLimitsOfShape	—	instHasLimitProd hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc limitUncurryIsoLimitCompLim_hom_π_π HasLimit.isoOfNatIso_hom_π CategoryTheory.Category.comp_id
limitIsoLimitCurryCompLim_hom_π_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.prod' instHasLimitProd CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.curry lim CategoryTheory.Iso.hom limitIsoLimitCurryCompLim limit.π hasLimitOfHasLimitsOfShape	—	instHasLimitProd hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitIsoLimitCurryCompLim_hom_π_π
limitIsoLimitCurryCompLim_inv_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor.curry lim instHasLimitProd CategoryTheory.Iso.inv limitIsoLimitCurryCompLim limit.π hasLimitOfHasLimitsOfShape	—	instHasLimitProd hasLimitOfHasLimitsOfShape CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc limitIsoLimitCurryCompLim_hom_π_π
limitIsoLimitCurryCompLim_inv_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor.curry lim instHasLimitProd CategoryTheory.Iso.inv limitIsoLimitCurryCompLim limit.π hasLimitOfHasLimitsOfShape	—	instHasLimitProd hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitIsoLimitCurryCompLim_inv_π
limitUncurryIsoLimitCompLim_hom_π_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.comp lim CategoryTheory.Iso.hom limitUncurryIsoLimitCompLim limit.π hasLimitOfHasLimitsOfShape	—	hasLimitOfHasLimitsOfShape limit.lift_π_assoc limit.lift_π
limitUncurryIsoLimitCompLim_hom_π_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.comp lim CategoryTheory.Iso.hom limitUncurryIsoLimitCompLim limit.π hasLimitOfHasLimitsOfShape	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitUncurryIsoLimitCompLim_hom_π_π
limitUncurryIsoLimitCompLim_inv_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category lim CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor.uncurry CategoryTheory.Iso.inv limitUncurryIsoLimitCompLim limit.π hasLimitOfHasLimitsOfShape	—	hasLimitOfHasLimitsOfShape CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc limitUncurryIsoLimitCompLim_hom_π_π
limitUncurryIsoLimitCompLim_inv_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category lim CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor.uncurry CategoryTheory.Iso.inv limitUncurryIsoLimitCompLim limit.π hasLimitOfHasLimitsOfShape	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitUncurryIsoLimitCompLim_inv_π

CategoryTheory.Limits.DiagramOfCocones

Definitions

Name	Category	Theorems
coconePoints 📖	CompOp	7 math math: mkOfHasColimits_coconePoints, CategoryTheory.Limits.coconeOfCoconeCurry_pt, coconePoints_map, coconePoints_obj, CategoryTheory.Limits.coconeOfCoconeUncurry_pt, CategoryTheory.Limits.coconeOfCoconeUncurry_ι_app, CategoryTheory.Limits.coconeOfCoconeCurry_ι_app
map 📖	CompOp	4 math math: coconePoints_map, comp, mkOfHasColimits_map_hom, id
mkOfHasColimits 📖	CompOp	3 math math: mkOfHasColimits_coconePoints, mkOfHasColimits_obj, mkOfHasColimits_map_hom
obj 📖	CompOp	7 math math: coconePoints_map, mkOfHasColimits_obj, comp, coconePoints_obj, id, CategoryTheory.Limits.coconeOfCoconeUncurry_ι_app, CategoryTheory.Limits.coconeOfCoconeCurry_ι_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconePoints_map 📖	mathematical	—	CategoryTheory.Functor.map coconePoints CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.Cocones.precompose map	—	—
coconePoints_obj 📖	mathematical	—	CategoryTheory.Functor.obj coconePoints CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor CategoryTheory.Functor.category obj	—	—
comp 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.Cocones.precompose CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct map CategoryTheory.Limits.Cocone.pt	—	—
id 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.Cocones.precompose CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct map CategoryTheory.Limits.Cocone.pt	—	—
mkOfHasColimits_coconePoints 📖	mathematical	—	coconePoints mkOfHasColimits CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.colim	—	—
mkOfHasColimits_map_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.colimit.cocone CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.Cocones.precompose CategoryTheory.Functor.map map mkOfHasColimits CategoryTheory.Limits.colim	—	—
mkOfHasColimits_obj 📖	mathematical	—	obj mkOfHasColimits CategoryTheory.Limits.colimit.cocone CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category	—	—

CategoryTheory.Limits.DiagramOfCones

Definitions

Name	Category	Theorems
conePoints 📖	CompOp	7 math math: CategoryTheory.Limits.coneOfConeCurry_pt, CategoryTheory.Limits.coneOfConeCurry_π_app, conePoints_map, conePoints_obj, CategoryTheory.Limits.coneOfConeUncurry_π_app, CategoryTheory.Limits.coneOfConeUncurry_pt, mkOfHasLimits_conePoints
map 📖	CompOp	4 math math: id, mkOfHasLimits_map_hom, conePoints_map, comp
mkOfHasLimits 📖	CompOp	3 math math: mkOfHasLimits_map_hom, mkOfHasLimits_obj, mkOfHasLimits_conePoints
obj 📖	CompOp	7 math math: id, CategoryTheory.Limits.coneOfConeCurry_π_app, conePoints_map, mkOfHasLimits_obj, conePoints_obj, CategoryTheory.Limits.coneOfConeUncurry_π_app, comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.Cones.postcompose CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map CategoryTheory.Limits.Cone.pt	—	—
conePoints_map 📖	mathematical	—	CategoryTheory.Functor.map conePoints CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.Cones.postcompose obj map	—	—
conePoints_obj 📖	mathematical	—	CategoryTheory.Functor.obj conePoints CategoryTheory.Limits.Cone.pt CategoryTheory.Functor CategoryTheory.Functor.category obj	—	—
id 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.Cones.postcompose CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj map CategoryTheory.Limits.Cone.pt	—	—
mkOfHasLimits_conePoints 📖	mathematical	—	conePoints mkOfHasLimits CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.lim	—	—
mkOfHasLimits_map_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.Cones.postcompose CategoryTheory.Functor.map CategoryTheory.Limits.limit.cone map mkOfHasLimits CategoryTheory.Limits.lim	—	—
mkOfHasLimits_obj 📖	mathematical	—	obj mkOfHasLimits CategoryTheory.Limits.limit.cone CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category	—	—

CategoryTheory.Limits.IsColimit

Definitions

Name	Category	Theorems
ofCoconeUncurry 📖	CompOp	—

CategoryTheory.Limits.IsLimit

Definitions

Name	Category	Theorems
ofConeOfConeUncurry 📖	CompOp	—

---

← Back to Index