Theorems · Inductive type · category theory
CategoryTheory.Limits.WalkingMulticospan
CategoryTheory.Limits.MulticospanShape → Type (max w w')
The type underlying the multiequalizer diagram.
- Cited by
- 199 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.MulticospanShapestatement · cited by 160
Cited by321
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.MulticospanIndex.multicospanstatement and proof · cited by 167
- CategoryTheory.Limits.Multifork.ιstatement · cited by 55
- CategoryTheory.Limits.Multifork.ofιproof · cited by 21
- CategoryTheory.GrothendieckTopology.plusCompIsostatement and proof · cited by 20
- CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkstatement · cited by 11
- CategoryTheory.GrothendieckTopology.sheafifyCompIsostatement and proof · cited by 11
- CategoryTheory.Limits.Multifork.conditionstatement and proof · cited by 10
- CategoryTheory.Limits.MulticospanIndex.toPiForkFunctorstatement · cited by 9
- CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctorstatement · cited by 9
- CategoryTheory.GrothendieckTopology.Plus.mkstatement and proof · cited by 9
- CategoryTheory.Meq.equivstatement and proof · cited by 8
- CategoryTheory.GrothendieckTopology.diagramCompIsostatement and proof · cited by 8
Showing the 200 most cited of 321.