Theorems · Inductive type · algebraic topology
SSet.Subcomplex.N
{X : SSet} → X.Subcomplex → Type uThe type of nondegenerate simplices which do not belong to a given subcomplex of a simplicial set.
- Cited by
- 155 results in Mathlib
- Foundations
- Depth 33 from the axioms, rests on 272 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SSetstatement · cited by 1,283
- SSet.Subcomplexstatement · cited by 461
Cited by227
Results whose statement or proof uses this declaration.
- SSet.Subcomplex.N.toNstatement and proof · cited by 126
- SSet.Subcomplex.Pairing.IIstatement · cited by 58
- SSet.Subcomplex.N.caststatement and proof · cited by 33
- SSet.Subcomplex.Pairing.pstatement · cited by 32
- SSet.prodStdSimplex.pairingCore.IsIndexstatement and proof · cited by 26
- SSet.Subcomplex.Pairing.Istatement · cited by 25
- SSet.Subcomplex.Pairing.AncestralRelstatement · cited by 22
- SSet.Subcomplex.Pairing.RankFunction.Cell.sstatement · cited by 21
- SSet.prodStdSimplex.pairingCore.minstatement and proof · cited by 18
- SSet.prodStdSimplex.pairingCore.IsType₂.φstatement and proof · cited by 14
- SSet.prodStdSimplex.pairingCore.IsType₂statement and proof · cited by 14
- SSet.Subcomplex.PairingCore.type₁statement · cited by 13
Showing the 200 most cited of 227.