δ_one_mkOfSucc — Mathlib

English

For i ∈ Fin n, δ_1 ≫ mkOfSucc i equals the constant map to i.castSucc.

Русский

Для i ∈ Fin n композиция δ_1 после mkOfSucc i равна константному отображению к i.castSucc.

LaTeX

$$$\\delta_1 \\circ mkOfSucc i = SimplexCategory.const \\_ ⦋n⦌ i.castSucc.$$$

Lean4

@[simp]
theorem δ_one_mkOfSucc {n : ℕ} (i : Fin n) : δ 1 ≫ mkOfSucc i = SimplexCategory.const _ ⦋n⦌ i.castSucc :=
  by
  ext x
  fin_cases x
  rfl

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