Theorems · Definition · category theory
CategoryTheory.Limits.Fan
{β : Type w} → {C : Type u} → [CategoryTheory.Category.{v, u} C] → (β → C) → Type (max (max w u) v)A fan over f : β → C consists of a collection of maps from an object P to every f b.
- Cited by
- 52 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Limits.Coneproof · cited by 710
- CategoryTheory.Discrete.functorproof · cited by 633
Cited by104
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.Fan.mkstatement · cited by 46
- CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimitstatement and proof · cited by 29
- CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimitstatement and proof · cited by 29
- CategoryTheory.Limits.Fan.projstatement and proof · cited by 28
- CategoryTheory.Limits.opCoproductIsoProduct'statement and proof · cited by 9
- CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctorstatement and proof · cited by 9
- CategoryTheory.Limits.MulticospanIndex.toPiForkFunctorstatement and proof · cited by 9
- CategoryTheory.Limits.Fan.IsLimit.liftstatement and proof · cited by 7
- CategoryTheory.Limits.Multifork.ofPiForkstatement and proof · cited by 6
- CategoryTheory.Limits.Multifork.toPiForkstatement and proof · cited by 6
- CategoryTheory.Limits.opProductIsoCoproduct'statement and proof · cited by 4
- CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_projstatement and proof · cited by 4