Mathlib Map

Theorems · Inductive type · category theory

CategoryTheory.Limits.WalkingPair

Type

The type of objects for the diagram indexing a binary (co)product.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Cited by
1,319 results in Mathlib
Foundations
Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.Limits.pair · cited by 536Limits.pairCategoryTheory.Limits.WalkingCospan · cited by 496Limits.WalkingCospanCategoryTheory.Limits.cospan · cited by 467Limits.cospanCategoryTheory.Limits.WalkingSpan · cited by 300Limits.WalkingSpanCategoryTheory.Limits.span · cited by 294Limits.spanCategoryTheory.Limits.PullbackCone.mk · cited by 203PullbackCone.mkCategoryTheory.Limits.PullbackCone.mk_π_app · cited by 120PullbackCone.mk_π_appCategoryTheory.Limits.PullbackCone.fst · cited by 118PullbackCone.fstCategoryTheory.Limits.PullbackCone.snd · cited by 113PullbackCone.sndCategoryTheory.Limits.BinaryFan.mk · cited by 112BinaryFan.mkCategoryTheory.Limits.HasBinaryCoproducts · cited by 98Limits.HasBinaryCoproductsCategoryTheory.Limits.PushoutCocone.mk · cited by 89PushoutCocone.mkCategoryTheory.Limits.BinaryCofan.mk · cited by 83BinaryCofan.mkCategoryTheory.Limits.HasBinaryProducts · cited by 79Limits.HasBinaryProductsCategoryTheory.Limits.WalkingPair.casesOn · cited by 59WalkingPair.casesOnLimits.WalkingPairCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by1,844

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 1,844.