mapMono_δ₀' — Mathlib

English

For a morphism i that is δ₀ in SimplexCategory, i must coincide with the first face δ₀; equivalently, among epis, i is δ₀ if and only if i equals δ₀.

Русский

Для морфизма i, являющегося δ₀ в SimplexCategory, i должен быть равен первой лицевой грани δ₀; то есть среди эпиморфизмов i равняется δ₀.

LaTeX

$$$Isδ₀(i) \iff i = δ_0$$$

Lean4

theorem mapMono_δ₀' (i : Δ' ⟶ Δ) [Mono i] (hi : Isδ₀ i) : mapMono K i = K.d Δ.len Δ'.len :=
  by
  unfold mapMono
  suffices Δ ≠ Δ' by simp only [dif_neg this, dif_pos hi]
  rintro rfl
  simpa only [left_eq_add, Nat.one_ne_zero] using hi.1

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