map_zero_succ_succ — Mathlib

English

The Precomp.obj function shifts the indexing by inserting X at the zeroth position and shifting the rest of the indices.

Русский

Функция Precomp.obj сдвигает индексы, вставляя X в нулевую позицию и сдвигая остальные индексы.

LaTeX

$$$\text{obj} : Fin (n + 1 + 1) \to C,\ x\mapsto \begin{cases} X & \text{if } x = ⟨0, -⟩ \\ F.obj' i & \text{if } x = ⟨i+1, -⟩ \end{cases}$$$

Lean4

@[simp]
theorem map_zero_succ_succ (j : ℕ) (hj : j + 2 < n + 1 + 1) : map F f 0 ⟨j + 2, hj⟩ (by simp) = f ≫ F.map' 0 (j + 1) :=
  rfl

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