Theorems · Theorem · algebraic topology
SSet.horn_obj_zero
∀ (n : ℕ) (i : Fin (n + 3)), (SSet.horn (n + 2) i).obj (Opposite.op { len := 0 }) = ⊤- Cited by
- 0 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites30
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
- Finsetproof · cited by 13,712
- Top.topstatement · cited by 9,680
- Oppositestatement · cited by 8,081
- Set.Elemproof · cited by 7,166
- Finset.univproof · cited by 3,473
- LE.le.transproof · cited by 3,151
- Compl.complproof · cited by 2,925
- Set.iUnionproof · cited by 2,483
- Finset.cardproof · cited by 2,327
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.