English
If a commutative square and an isomorphism i: P ≅ pullback f g relate fst,snd to fst',snd' via compatible maps, then fst',snd' form a pullback of f,g.
Русский
Если дан квадр-образ commutSq и изоморфизм i: P ≅ pullback f g, связывающий fst,snd с fst',snd' через совместимые стрелки, то fst',snd' образуют предел по f,g.
LaTeX
$$$ \text{CommSq fst snd f g} \land i : P \cong pullback f g \land (i.hom \circ pullback.fst f g = fst) \land (i.hom \circ pullback.snd f g = snd) \Rightarrow IsPullback fst snd f g $$$
Lean4
theorem of_iso_pullback (h : CommSq fst snd f g) [HasPullback f g] (i : P ≅ pullback f g)
(w₁ : i.hom ≫ pullback.fst _ _ = fst) (w₂ : i.hom ≫ pullback.snd _ _ = snd) : IsPullback fst snd f g :=
of_isLimit' h
(Limits.IsLimit.ofIsoLimit (limit.isLimit _)
(@PullbackCone.ext _ _ _ _ _ _ _ (PullbackCone.mk _ _ _) _ i w₁.symm w₂.symm).symm)
