Theorems · Theorem · algebraic topology
SSet.stdSimplex.opObjEquiv_opObjEquiv_symm_apply
∀ {d n : ℕ} (f : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })) (i : Fin (d + 1)),
(SSet.opObjEquiv (SSet.stdSimplex.opObjEquiv.symm f)) i = (f i.rev).rev- Cited by
- 0 results in Mathlib
- Foundations
- Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- Equivstatement · cited by 8,337
- Oppositestatement · cited by 8,081
- Equiv.symmstatement · cited by 3,681
- SimplexCategorystatement · cited by 2,204
- SSetstatement · cited by 1,283
- SSet.stdSimplexstatement and proof · cited by 499
- SSet.opstatement · cited by 33
- SSet.opObjEquivstatement · cited by 26
- SSet.stdSimplex.opObjEquivstatement · cited by 6
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.