Theorems · Definition · category theory

CategoryTheory.Limits.Fan.mk

{β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} → (P : C) → ((b : β) → P ⟶ f b) → CategoryTheory.Limits.Fan f

A fan over f : β → C consists of a collection of maps from an object P to every f b.

Defined in: Mathlib.CategoryTheory.Limits.Shapes.Products
Cited by: 46 results in Mathlib
Foundations: Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

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
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Discreteproof · cited by 2,447
CategoryTheory.Discrete.asproof · cited by 269
CategoryTheory.Discrete.natTransproof · cited by 57
CategoryTheory.Limits.Fanstatement · cited by 52

Cited by79

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.Pi.liftproof · cited by 53
CategoryTheory.Limits.biproduct.liftproof · cited by 31
CategoryTheory.Limits.biproduct.lift_πproof · cited by 19
CategoryTheory.Limits.productIsProductstatement · cited by 11
CategoryTheory.Limits.Pi.map'_comp_πproof · cited by 9
CategoryTheory.Limits.Types.pi_lift_π_applyproof · cited by 9
CategoryTheory.Limits.piComparison_comp_πproof · cited by 9
CategoryTheory.Limits.Fan.IsLimit.liftproof · cited by 7
CategoryTheory.Limits.Bicone.ofLimitConeproof · cited by 5
CategoryTheory.Limits.Fan.IsLimit.facproof · cited by 4
TopCat.piFanproof · cited by 3
CategoryTheory.Limits.biproduct.isoProduct_homproof · cited by 3