English
If F reflects the limit for a cospan and maps e to a pullback, then IsPullback f g h i holds given F.map f, F.map g, ... and e is a witness of the equation.
Русский
Если F отражает предел для коспана и отображает e в искомое, тогда IsPullback f g h i выполняется при отображении F.map f, F.map g и т.д.
LaTeX
$$$ [\\operatorname{ReflectsLimit}(\\mathrm{cospan}(h,i)) F] (e : f\\!\\to\\!h = g\\!\\to\\!i) (H : \\operatorname{IsPullback}(F.map f,F.map g,F.map h,F.map i)) \\Rightarrow \\operatorname{IsPullback}(f,g,h,i) $$$
Lean4
theorem of_map [ReflectsLimit (cospan h i) F] (e : f ≫ h = g ≫ i)
(H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)) : IsPullback f g h i :=
by
refine ⟨⟨e⟩, ⟨isLimitOfReflects F <| ?_⟩⟩
refine (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)).symm H.isLimit
exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _).symm,
(Category.comp_id _).trans (Category.id_comp _).symm]
