Theorems · Inductive type · category theory
SSet.innerHornInclusions
CategoryTheory.MorphismProperty SSet
The family of morphisms in SSet which consists of inner horn inclusions
Λ[n, i].ι : Λ[n, i] ⟶ Δ[n] (for 0 < i < n).
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Oppositestatement · cited by 8,081
- SimplexCategorystatement · cited by 2,204
- CategoryTheory.MorphismPropertystatement · cited by 2,179
- SSetstatement · cited by 1,283
Cited by15
Results whose statement or proof uses this declaration.
- SSet.innerFibrationsproof · cited by 10
- SSet.horn_ι_mem_innerHornInclusionsstatement · cited by 4
- SSet.innerAnodyneExtensions_eq_llp_rlpstatement · cited by 4
- SSet.quasicategory_iff_innerFibrationproof · cited by 2
- SSet.innerHornInclusions_le_Jstatement and proof · cited by 2
- SSet.innerAnodyneExtensions.horn_ιproof · cited by 1
- SSet.innerFibration_pullbackObjObjπproof · cited by 1
- SSet.innerHornInclusions.casesOnstatement and proof · cited by 1
- SSet.innerHornInclusions_eq_iSupstatement and proof · cited by 0
- SSet.innerHornInclusions_le_monomorphismsstatement · cited by 0
- SSet.innerHornInclusions.recOnstatement and proof · cited by 0
- SSet.Quasicategory.from_innerFibrationsproof · cited by 0