English
If x = y in the simplex category, then eqToHom h induces the same order-hom as the corresponding castOrderIso embedding on len+1.
Русский
Если x = y в симплексной категории, то отображение eqToHom позволяет получить такое же отображение порядка, как и соответствующая вставка через castOrderIso на len+1.
LaTeX
$$∀ {x y} (h : x = y), SimplexCategory.Hom.toOrderHom (eqToHom h) = (Fin.castOrderIso (congrArg (fun t ↦ t.len + 1) h)).toOrderEmbedding.toOrderHom$$
Lean4
theorem δ_comp_δ' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) :
δ i ≫ δ j = δ (j.pred fun (hj : j = 0) => by simp [hj, Fin.not_lt_zero] at H) ≫ δ (Fin.castSucc i) :=
by
rw [← δ_comp_δ]
· rw [Fin.succ_pred]
·
simpa only [Fin.le_iff_val_le_val, ← Nat.lt_succ_iff, Nat.succ_eq_add_one, ← Fin.val_succ, j.succ_pred,
Fin.lt_iff_val_lt_val] using H
