Theorems · Theorem · algebraic topology
SSet.Truncated.HomotopyCategory.mk_surjective
∀ {V : SSet.Truncated 2}, Function.Surjective SSet.Truncated.HomotopyCategory.mk- Cited by
- 2 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objstatement · cited by 19,642
- Oppositestatement · cited by 8,081
- SimplexCategorystatement · cited by 2,204
- SimplexCategory.lenstatement · cited by 542
- SimplexCategory.Truncatedstatement · cited by 236
- SSet.Truncatedstatement and proof · cited by 214
- CategoryTheory.Pathsproof · cited by 82
- SSet.Truncated.HomotopyCategorystatement and proof · cited by 54
- SSet.Truncated.HomotopyCategory.mkstatement · cited by 37
- CategoryTheory.Cat.FreeReflproof · cited by 34
- SSet.OneTruncation₂proof · cited by 26
- CategoryTheory.Quotient.casesOnproof · cited by 8
Cited by2
Results whose statement or proof uses this declaration.
- SSet.Truncated.HomotopyCategory.extproof · cited by 0
- SSet.Truncated.HomotopyCategory.cases_onproof · cited by 0