pullbackRightPullbackFstIso_inv_fst

English

The inverse of the right pullback iso composed with fst' equals fst of the composed arrow f' ∘ f.

Русский

Обратный к правому изоморфизму пулбэпа, композиция fst' равна fst с пары f'∘f.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem pullbackRightPullbackFstIso_inv_fst :
    (pullbackRightPullbackFstIso f g f').inv ≫ pullback.fst f' (pullback.fst f g) = pullback.fst (f' ≫ f) g :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.left

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