mem_nerve_degenerate_of_eq — Mathlib

English

If in a simplex s of the nerve, two consecutive vertices are equal (i.castSucc = i.succ), then s lies in the degenerate part of the nerve.

Русский

Если в симплексe nerve две последовательные вершины равны (i.castSucc = i.succ), то s лежит в degenerate части нерва.

LaTeX

$$$\text{If } s.obj i.castSucc = s.obj i.succ,\; s \in \mathrm{degenerate}(n+1)$$$

Lean4

theorem mem_nerve_degenerate_of_eq (s : (nerve X) _⦋n + 1⦌) {i : Fin (n + 1)} (hi : s.obj i.castSucc = s.obj i.succ) :
    s ∈ (nerve X).degenerate (n + 1) :=
  by
  simp only [nerve_obj, SSet.degenerate_eq_iUnion_range_σ, Set.mem_iUnion]
  exact ⟨i, by rwa [mem_range_nerve_σ_iff]⟩

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