Theorems · Definition · category theory
CategoryTheory.Limits.MultispanShape.fst
(self : CategoryTheory.Limits.MultispanShape) → self.L → self.R
the first map L → R
- Cited by
- 50 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
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.Limits.MultispanShape.Rstatement · cited by 133
- CategoryTheory.Limits.MultispanShape.Lstatement · cited by 129
- CategoryTheory.Limits.MultispanShapestatement and proof · cited by 102
Cited by71
Results whose statement or proof uses this declaration.
- CategoryTheory.GlueData.diagramproof · cited by 68
- CategoryTheory.Limits.MultispanIndex.fststatement · cited by 40
- CategoryTheory.Limits.MultispanIndex.fstSigmaMapOfIsColimitproof · cited by 29
- CategoryTheory.Limits.Multicofork.ofπstatement and proof · cited by 15
- CategoryTheory.Limits.Multicoequalizer.descstatement and proof · cited by 10
- CategoryTheory.Limits.Multicofork.conditionstatement and proof · cited by 9
- CategoryTheory.Limits.Multicoequalizer.hom_extproof · cited by 8
- TopCat.GlueData.ι_eq_iff_relproof · cited by 4
- CategoryTheory.Limits.Multicoequalizer.conditionstatement · cited by 3
- CategoryTheory.Limits.Multicoequalizer.π_descstatement and proof · cited by 3
- CategoryTheory.Limits.Multicoequalizer.π_desc_assocstatement and proof · cited by 3
- CategoryTheory.Limits.Multicofork.fst_app_rightstatement and proof · cited by 3