instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions

English

If HasExplicitFiniteCoproducts P and HasExplicitPullbacksOfInclusions P hold, then CompHausLike HasPullbacksOfInclusions P.

Русский

Если выполняются HasExplicitFiniteCoproducts P и HasExplicitPullbacksOfInclusions P, то CompHausLike имеет HasPullbacksOfInclusions P.

LaTeX

$$$\\forall P,\\ [HasExplicitFiniteCoproducts\\ P]\\ [HasExplicitPullbacksOfInclusions\\ P]\\Rightarrow \\mathrm{HasPullbacksOfInclusions}(\\mathrm{CompHausLike} P)$$$

Lean4

instance [HasExplicitPullbacksOfInclusions P] : HasPullbacksOfInclusions (CompHausLike P) where
  hasPullbackInl _ := inferInstance

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