isoIsPullback_inv_snd — Mathlib

English

Let h and h' be pullbacks of f and g along snd and snd'. Then the inverse of the isomorphism between the pullbacks, composed with snd, equals snd'.

Русский

Пусть две структуры предела по f, g вдоль snd и snd'; тогда inv изоморфизма между пределами, сопоставленный с snd, равен snd'.

LaTeX

$$$ (h.isoIsPullback X Y h').inv \circ snd = snd' $$$

Lean4

@[reassoc (attr := simp)]
theorem isoIsPullback_inv_snd (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :
    (h.isoIsPullback _ _ h').inv ≫ snd = snd' := by simp only [Iso.inv_comp_eq, isoIsPullback_hom_snd]

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