isoPullback_inv_snd — Mathlib

English

The inverse of the pullback iso composed with snd equals the canonical pullback snd map.

Русский

Обратный изоморфизм предела по диаграмме, композированный с snd, равен pullback.snd.

LaTeX

$$$ h.isoPullback.inv \circ snd = pullback.snd f g $$$

Lean4

@[reassoc (attr := simp)]
theorem isoPullback_inv_snd (h : IsPullback fst snd f g) [HasPullback f g] :
    h.isoPullback.inv ≫ snd = pullback.snd _ _ := by simp [Iso.inv_comp_eq]

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