English
If HasExplicitFiniteCoproducts P and HasExplicitPullbacksOfInclusions P, then CompHausLike hasPullbacksOfInclusions.
Русский
Если HasExplicitFiniteCoproducts P и HasExplicitPullbacksOfInclusions P, то CompHausLike имеет HasPullbacksOfInclusions.
LaTeX
$$$\\forall P, [HasExplicitFiniteCoproducts P] [HasExplicitPullbacksOfInclusions P] \\Rightarrow \\text{HasPullbacksOfInclusions}(\\mathrm{CompHausLike} P)$$$
Lean4
/-- The functor to `TopCat` preserves pullbacks of inclusions if they exist. -/
noncomputable instance [HasExplicitPullbacksOfInclusions P] : PreservesPullbacksOfInclusions (compHausLikeToTop P) :=
{
preservesPullbackInl := by
intro X Y Z f
infer_instance }
