mem_nonDegenerate_iff_mono — Mathlib

English

An s ∈ Δ[n].nonDegenerate d iff the underlying map objEquiv s is mono.

Русский

s ∈ Δ[n].nonDegenerate d эквивалентно тому, что отображение objEquiv s является моно.

LaTeX

$$s ∈ Δ[n].nonDegenerate d ⇔ Mono (objEquiv s)$$

Lean4

theorem mem_nonDegenerate_iff_mono {n d : ℕ} (s : (Δ[n] : SSet.{u}) _⦋d⦌) :
    s ∈ Δ[n].nonDegenerate d ↔ Mono (objEquiv s) :=
  by
  rw [mem_nonDegenerate_iff_strictMono, SimplexCategory.mono_iff_injective]
  refine ⟨fun h ↦ h.injective, fun h ↦ ?_⟩
  rw [Fin.strictMono_iff_lt_succ]
  intro i
  obtain h' | h' := (stdSimplex.monotone_apply s i.castSucc_le_succ).lt_or_eq
  · exact h'
  · simpa [Fin.ext_iff] using h h'

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