arrowSucc_extendToSucc — Mathlib

English

Equality of two-way map expressions using the composed indices.

Русский

Равенство двух выражений отображения с использованием скомпонованных индексов.

LaTeX

$$$\\text{ExtendToSucc.map}\\; hj\\; F\\; τ\\; i_1\\; i_3\\; \\dots = \\text{ExtendToSucc.map}(i_1,i_2) \\circ \\text{ExtendToSucc.map}(i_2,i_3)$$$

Lean4

theorem arrowSucc_extendToSucc : arrowSucc (extendToSucc hj F τ) j (Order.lt_succ_of_not_isMax hj) = Arrow.mk τ := by
  simp [arrowSucc, arrowMap, extendToSucc_map_le_succ, extendToSuccObjIso, extendToSucc.objIso, extendToSuccObjSuccIso,
    extendToSucc.objSuccIso]

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