arrowMap_extendToSucc — Mathlib

English

The map commutes with composition in a way compatible with the previous lemmas.

Русский

Отображение коммутирует с композициями в согласии с предыдущими леммами.

LaTeX

$$$\\text{ExtendToSucc.map}(i_1,i_3,h_{12}h_{23},h)=\\text{ExtendToSucc.map}(i_1,i_2,h_{12},h_{23}.trans h) \\, ≫ \\, \\text{ExtendToSucc.map}(i_2,i_3,h_{23},h)$$$

Lean4

theorem arrowMap_extendToSucc (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
    arrowMap (extendToSucc hj F τ) i₁ i₂ hi (hi₂.trans (Order.le_succ j)) = arrowMap F i₁ i₂ hi hi₂ := by
  simp [arrowMap, extendToSucc_map hj F τ i₁ i₂ hi hi₂, extendToSuccObjIso, extendToSucc.objIso]

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