English
The order on the simplices of a simplicial set is given by subcomplex inclusion: s ≤ t if and only if the subcomplex generated by s is contained in the subcomplex generated by t.
Русский
Порядок на симплексах симплициального множества задаётся вложенностью подслоя: s ≤ t тогда и только тогда, когда подслой, порождаемый s, содержится внутри подслоя, порождаемого t.
LaTeX
$$$\text{Preorder on } X.S:\ s \le t \iff (\text{subcomplex generated by } s) \subseteq (\text{subcomplex generated by } t)$$$
Lean4
/-- If `s : X.S` and `t : X.S` are simplices of a simplicial set, `s ≤ t` means
that the subcomplex generated by `s` is contained in the subcomplex generated by `t`,
see `SSet.S.le_def` and `SSet.S.le_iff`. Note that the
category structure on `X.S` induced by this preorder is not
the "category of simplices" of `X` (which is see `X.Elementsᵒᵖ`);
see `SSet.S.le_iff_nonempty_hom` for the precise relation. -/
instance : Preorder X.S :=
Preorder.lift subcomplex
