Theorems · Theorem · category theory
CategoryTheory.nerve.nonempty_compStruct_iff
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x₀ x₁ x₂ : C} (f₀₁ : x₀ ⟶ x₁) (f₁₂ : x₁ ⟶ x₂) (f₀₂ : x₀ ⟶ x₂),
Nonempty
((CategoryTheory.nerve.edgeMk f₀₁).CompStruct (CategoryTheory.nerve.edgeMk f₁₂)
(CategoryTheory.nerve.edgeMk f₀₂)) ↔
CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂- Cited by
- 1 results in Mathlib
- Foundations
- Depth 66 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.
Cites39
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objproof · cited by 19,642
- CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
- CategoryTheory.Functor.mapproof · cited by 8,698
- Equivstatement · cited by 8,337
- CategoryTheory.CategoryStruct.idproof · cited by 6,235
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- Equiv.symmstatement and proof · cited by 3,681
- CategoryTheory.Category.comp_idproof · cited by 2,119
- CategoryTheory.Category.id_compproof · cited by 1,998
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.nerve.homEquiv_compproof · cited by 0