Theorems · Theorem · algebraic topology
SSet.boundary_eq_iSup
∀ (n : ℕ), SSet.boundary n = ⨆ i, SSet.stdSimplex.face {i}ᶜ- Cited by
- 4 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.
Cites25
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- Finsetstatement · cited by 13,712
- Oppositestatement and proof · cited by 8,081
- Set.ofPredproof · cited by 6,101
- Compl.complstatement and proof · cited by 2,925
- Set.iUnionproof · cited by 2,483
- iSupstatement · cited by 2,415
- Set.extproof · cited by 2,266
- Opposite.unopproof · cited by 2,231
- SimplexCategorystatement and proof · cited by 2,204
- SSetstatement · cited by 1,283
Cited by4
Results whose statement or proof uses this declaration.
- SSet.face_singleton_compl_le_boundaryproof · cited by 2
- SSet.stdSimplex.notMem_boundaryproof · cited by 1
- SSet.boundary.hom_extproof · cited by 0
- SSet.mem_boundary_iff_notMem_rangeproof · cited by 0