map_eq — Mathlib

English

Equality between two ways of composing maps in extendToSucc, given i₁ ≤ i₂ ≤ j.

Русский

Равенство двух способов композиции отображений в extendToSucc при i₁ ≤ i₂ ≤ j.

LaTeX

$$$\\text{ExtendToSucc.map}\\; hj\\; F\\; τ\\; i_1\\ i_2\\ hi\\ hi_2 = (\\text{objIso}\\; F\\ X\\ ⟨i_1,\\dots⟩) \\to\\circ F.map\\circ (\\text{objIso}\\; F\\ X\\ ⟨i_2,\\dots⟩) $$$

Lean4

theorem map_eq (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
    map hj F τ i₁ i₂ hi (hi₂.trans (Order.le_succ j)) =
      (objIso F X ⟨i₁, hi.trans hi₂⟩).hom ≫ F.map (homOfLE hi) ≫ (objIso F X ⟨i₂, hi₂⟩).inv :=
  dif_pos hi₂

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