extendToSucc_map — Mathlib

English

Compatibility of map with indices when taking le_succ.

Русский

Совместимость отображения с индексами при взятии le_succ.

LaTeX

$$$\\text{extendToSuccObjIso}\\; i_1\\ (hi.trans hi_2) \\quad \\text{and} \\quad hi_2$$

Lean4

theorem extendToSucc_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
    (extendToSucc hj F τ).map
        (homOfLE hi : ⟨i₁, hi.trans (hi₂.trans (Order.le_succ j))⟩ ⟶ ⟨i₂, hi₂.trans (Order.le_succ j)⟩) =
      (extendToSuccObjIso hj F τ i₁ (hi.trans hi₂)).hom ≫ F.map (homOfLE hi) ≫ (extendToSuccObjIso hj F τ i₂ hi₂).inv :=
  by rw [← extendToSuccObjIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

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