Theorems · Inductive type · category theory
CategoryTheory.Limits.WalkingMultispan
CategoryTheory.Limits.MultispanShape → Type (max w w')
The type underlying the multicoequalizer diagram.
- Cited by
- 151 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Limits.MultispanShapestatement · cited by 102
Cited by229
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.MultispanIndex.multispanstatement and proof · cited by 139
- CategoryTheory.Limits.Multicofork.πstatement · cited by 50
- CategoryTheory.Limits.Multicofork.ofπproof · cited by 15
- CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkstatement · cited by 11
- CategoryTheory.Limits.Multicofork.conditionstatement and proof · cited by 9
- CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctorstatement · cited by 9
- CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctorstatement · cited by 9
- CategoryTheory.GlueData.gluedIsostatement · cited by 9
- CategoryTheory.Limits.Multicoequalizer.hom_extproof · cited by 8
- SSet.horn.isColimitstatement · cited by 8
- CategoryTheory.GlueData.diagramIsostatement and proof · cited by 8
- CategoryTheory.GlueData.ι_gluedIso_invstatement · cited by 8
Showing the 200 most cited of 229.