extendToSucc_map_le_succ — Mathlib

English

Alternative expression for map via lemmas: eq, trans, and id rules.

Русский

Альтернативное выражение отображения через леммы: равенство, переходы и правила для единицы.

LaTeX

$$$\\text{map}_{alt} = (\\text{objIso}\\; F\\; X) \\circ F.map \\circ (\\text{objIso}\\; F\\; X)^{-1}$$$

Lean4

theorem extendToSucc_map_le_succ :
    (extendToSucc hj F τ).map (homOfLE (Order.le_succ j)) =
      (extendToSuccObjIso hj F τ j (by simp)).hom ≫ τ ≫ (extendToSuccObjSuccIso hj F τ).inv :=
  extendToSucc.map_self_succ _ _ _

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