English
Let F be a composable arrow sequence of length n in a category C, and let f be a morphism X → F.left. For all i, j with suitable index bounds and with i + 1 ≤ j + 1, the (i+1, j+1) entry of the precomposition map equals the original map′ entry: map F f (i+1, hi) (j+1, hj) hij = F.map′ i j.
Русский
Пусть F задаёт последовательность композиционных стрелок длины n в категории C, и дано отображение f: X → F.left. Для всех допустимых i, j существует равенство: map F f (i+1, hi) (j+1, hj) hij = F.map′ i j.
LaTeX
$$$\\forall F\\ (f:X \\to F.left)\\ (i\\ j:\\mathbb{N})\\ (hi:\\ i+1 < n+1+1) (hj:\\ j+1 < n+1+1) (hij:\\ i+1 \\le j+1),\\quad map\\ F\\ f\\ ⟨i+1,hi⟩\\ ⟨j+1,hj⟩\\ hij = F.map' i j$$$
Lean4
@[simp]
theorem map_succ_succ (i j : ℕ) (hi : i + 1 < n + 1 + 1) (hj : j + 1 < n + 1 + 1) (hij : i + 1 ≤ j + 1) :
map F f ⟨i + 1, hi⟩ ⟨j + 1, hj⟩ hij = F.map' i j :=
rfl
