isoIsPullback_inv_fst — Mathlib

English

Let h and h' be two pullback structures of f and g along fst and fst'. Then the canonical isomorphism between the two pullbacks satisfies inv ∘ fst = fst'.

Русский

Пусть две структуры предела по f, g вдоль fst и fst' образуют два предела; тогда каноническое изоморфизм между этими пределами удовлетворяет равенству inv ∘ fst = fst'.

LaTeX

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

Lean4

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

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