Theorems · Theorem · order theory
PartialOrder.mem_nerve_nonDegenerate_iff_strictMono
∀ {X : Type u_1} [inst : PartialOrder X] {n : ℕ} (s : (CategoryTheory.nerve X).obj (Opposite.op { len := n })),
s ∈ (CategoryTheory.nerve X).nonDegenerate n ↔ StrictMono s.obj- Cited by
- 3 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PartialOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- Oppositestatement · cited by 8,081
- PartialOrderstatement and proof · cited by 6,410
- Opposite.unopstatement and proof · cited by 2,231
- SimplexCategorystatement · cited by 2,204
- StrictMonostatement and proof · cited by 706
- SimplexCategory.lenstatement and proof · cited by 542
- Set.mem_iUnionproof · cited by 212
- not_iff_notproof · cited by 159
- SSet.nonDegeneratestatement · cited by 106
- CategoryTheory.nervestatement and proof · cited by 68
Cited by3
Results whose statement or proof uses this declaration.
- SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquivproof · cited by 3
- SSet.stdSimplex.mem_nonDegenerate_iff_strictMonoproof · cited by 2
- PartialOrder.mem_nerve_nonDegenerate_iff_injectiveproof · cited by 1