Theorems · Definition · category theory
CategoryTheory.Limits.WalkingSpan.Hom.fst
CategoryTheory.Limits.WalkingSpan.zero ⟶ CategoryTheory.Limits.WalkingSpan.left
The left arrow of the walking span.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
- CategoryTheory.Limits.WalkingSpanstatement · cited by 300
- CategoryTheory.Limits.WalkingSpan.leftstatement · cited by 80
- CategoryTheory.Limits.WalkingSpan.zerostatement · cited by 25
Cited by23
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.diagramIsoSpanstatement · cited by 16
- CategoryTheory.Limits.PushoutCocone.conditionproof · cited by 15
- CategoryTheory.Limits.PushoutCocone.isoMkstatement · cited by 5
- CategoryTheory.Limits.PushoutCocone.condition_zeroproof · cited by 4
- CategoryTheory.Limits.PushoutCocone.coequalizer_extproof · cited by 3
- CategoryTheory.Limits.diagramIsoSpan_hom_appstatement · cited by 2
- CategoryTheory.Limits.PushoutCocone.ofCoconestatement · cited by 2
- CategoryTheory.Limits.spanIsoMkstatement and proof · cited by 2
- CategoryTheory.IsPushout.isVanKampen_iffproof · cited by 2
- CategoryTheory.Limits.Cocone.ofPushoutCoconestatement and proof · cited by 2
- CategoryTheory.Limits.spanHomMkstatement and proof · cited by 1
- CategoryTheory.Limits.diagramIsoSpan_inv_appstatement · cited by 0