English
A simplex s in the nerve is nondegenerate if and only if the vertex map s.obj is strictly monotone (strictly increasing).
Русский
Симплекс в нерве неdegenerate тогда и только тогда, когда отображение вершин s.obj строго монотонно (возрастает).
LaTeX
$$$ s \in (\mathrm{nerve}
X)\;\text{nonDegenerate } n \iff \text{StrictMono } s.\mathrm{obj}$$$
Lean4
theorem mem_nerve_nonDegenerate_iff_strictMono (s : (nerve X) _⦋n⦌) :
s ∈ (nerve X).nonDegenerate n ↔ StrictMono s.obj :=
by
obtain _ | n := n
· simpa using Subsingleton.strictMono _
· rw [← not_iff_not, ← SSet.mem_degenerate_iff_notMem_nonDegenerate, Fin.strictMono_iff_lt_succ,
SSet.degenerate_eq_iUnion_range_σ, Set.mem_iUnion]
simp only [mem_range_nerve_σ_iff, not_forall]
apply exists_congr
intro i
have := s.monotone i.castSucc_le_succ
grind [SimplexCategory.len_mk, lt_self_iff_false, LE.le.lt_or_eq]