mem_nerve_nonDegenerate_iff_strictMono

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]

Похожие утверждения