pullbackRightPullbackFstIso_inv_snd_snd

English

The inverse of the right pullback iso composed with the second projection twice yields the second projection again, expressing a consistency with the right-hand leg.

Русский

Обратный к правому изоморфизму пулбэпа, композиция с snd повторно возвращает snd.

LaTeX

$$$(\text{pullbackRightPullbackFstIso } f g f').inv \; ≫ \; \text{pullback.snd } _ _ ≫ \; \text{pullback.snd } _ _ = \text{pullback.snd } _ _.$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackRightPullbackFstIso_inv_snd_snd :
    (pullbackRightPullbackFstIso f g f').inv ≫ pullback.snd _ _ ≫ pullback.snd _ _ = pullback.snd _ _ :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.right

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