Theorems · Theorem · algebraic topology

SSet.stdSimplex.toSSetObj_app_const_zero

(CategoryTheory.ConcreteCategory.hom (SSet.stdSimplex.toSSetObjI.app (Opposite.op { len := 0 })))
    (SSet.stdSimplex.const 1 0 (Opposite.op { len := 0 })) =
  TopCat.toSSetObj₀Equiv.symm 0

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Cited by: 1 results in Mathlib
Foundations: Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites27

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
CategoryTheory.Functor.objstatement · cited by 19,642
CategoryTheory.CategoryStruct.compproof · cited by 17,999
Equivstatement · cited by 8,337
Oppositestatement · cited by 8,081
CategoryTheory.NatTrans.appstatement and proof · cited by 7,406
CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
Equiv.symmstatement and proof · cited by 3,681
TopCat.carrierstatement · cited by 3,184
SimplexCategorystatement · cited by 2,204
TopCatstatement · cited by 1,889
TypeCat.Funstatement · cited by 1,307

Cited by1

Results whose statement or proof uses this declaration.

SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μproof · cited by 1