mem_nerve_nonDegenerate_iff_injective

English

A simplex is nondegenerate in the nerve iff the vertex map s.obj is injective.

Русский

Симплекс в нерве неdegenerate тогда и только тогда, когда отображение вершин s.obj инъективно.

LaTeX

$$$ s \in (\mathrm{nerve} X).nonDegenerate n \iff \text{Function.Injective } s.obj$$$

Lean4

theorem mem_nerve_nonDegenerate_iff_injective (s : (nerve X) _⦋n⦌) :
    s ∈ (nerve X).nonDegenerate n ↔ Function.Injective s.obj :=
  by
  rw [mem_nerve_nonDegenerate_iff_strictMono]
  refine ⟨fun h ↦ h.injective, fun h i j hij ↦ ?_⟩
  obtain h' | h' := (s.monotone hij.le).lt_or_eq
  · exact h'
  · exact ((h h').not_lt hij).elim

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