pullbackLeftPullbackSndIso_hom_snd

English

In the pasting square, the inverse of the left iso composed with snd equals snd after pasting, expressing another facet of the commutativity of the pasted diagram.

Русский

В pasting-окне обратный к левому изоморфизму, скомпонованный со snd, равен snd после склейки, выражая еще одно свойство коммутативности рисунка.

LaTeX

$$$(\\mathrm{pullbackLeftPullbackSndIso}(f,g,g')).\\mathrm{inv} \\circ \\mathrm{pullback.snd} (f,\\; g) \;=\; \\mathrm{pullback.snd}(\\mathrm{pullback.snd}(f,g),g')$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackLeftPullbackSndIso_hom_snd :
    (pullbackLeftPullbackSndIso f g g').hom ≫ pullback.snd _ _ = pullback.snd _ _ :=
  IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right

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