Documentation
InfinityCosmos
.
ForMathlib
.
AlgebraicTopology
.
SimplicialSet
.
Monoidal
Search
return to top
source
Imports
Init
InfinityCosmos.ForMathlib.AlgebraicTopology.SimplexCategory
Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Imported by
InfinityCosmos
InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy
SSet
.
isTerminalDeltaZero
source
def
SSet
.
isTerminalDeltaZero
:
CategoryTheory.Limits.IsTerminal
(
stdSimplex
.
obj
(
SimplexCategory.mk
0
)
)
The object
Δ[0]
is terminal in
SSet
.
Equations
One or more equations did not get rendered due to their size.