Theorems · Definition · category theory
CategoryTheory.ComposableArrows.right
{C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {n : ℕ} → CategoryTheory.ComposableArrows C n → CThe rightmost object of F : ComposableArrows C n.
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound
- 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.ComposableArrowsstatement and proof · cited by 627
- CategoryTheory.ComposableArrows.obj'proof · cited by 94
Cited by25
Results whose statement or proof uses this declaration.
- CategoryTheory.ComposableArrows.homstatement · cited by 28
- CategoryTheory.ComposableArrows.ext₁statement and proof · cited by 16
- CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrowsstatement · cited by 5
- CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrowsstatement · cited by 3
- CategoryTheory.nerve.mk₁_homEquiv_applystatement · cited by 1
- CategoryTheory.nerve.nonempty_compStruct_iffproof · cited by 1
- CategoryTheory.nerve.right_edgestatement and proof · cited by 1
- CategoryTheory.nerve.δ₂_twoproof · cited by 1
- CategoryTheory.nerve.δ₂_zeroproof · cited by 1
- CategoryTheory.ComposableArrows.mk₁_homstatement · cited by 1
- CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_appstatement · cited by 0
- CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBotstatement · cited by 0