Theorems · Theorem · algebraic topology
SSet.horn_eq_iSup
∀ (n : ℕ) (i : Fin (n + 1)), SSet.horn n i = ⨆ j, SSet.stdSimplex.face {↑j}ᶜ- Cited by
- 9 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites32
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement · cited by 53,352
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- Finsetstatement · cited by 13,712
- Oppositestatement and proof · cited by 8,081
- Set.Elemstatement and proof · cited by 7,166
- Set.ofPredproof · cited by 6,101
- Set.rangeproof · cited by 4,705
- Set.univproof · cited by 3,945
- Compl.complstatement and proof · cited by 2,925
- Set.iUnionproof · cited by 2,483
- iSupstatement · cited by 2,415
Cited by9
Results whose statement or proof uses this declaration.
- SSet.horn.multicoequalizerDiagramproof · cited by 16
- SSet.face_le_hornproof · cited by 5
- SSet.horn_obj_eq_univproof · cited by 2
- SSet.horn₂₁.sqproof · cited by 1
- SSet.horn₂₂.sqproof · cited by 1
- SSet.horn.hom_extproof · cited by 1
- SSet.horn₂₀.sqproof · cited by 1
- SSet.horn_obj_zeroproof · cited by 0
- SSet.mem_horn_iff_notMem_rangeproof · cited by 0