instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions

English

If HasExplicitPullbacksOfInclusions and HasExplicitFiniteCoproducts hold, then CompHausLike P is finitary extensive.

Русский

Если выполняются HasExplicitPullbacksOfInclusions и HasExplicitFiniteCoproducts, то CompHausLike P является конечносшиваемым и экстенсивным.

LaTeX

$$$\\mathrm{FinitaryExtensive}(\\mathrm{CompHausLike}\ P)$$$

Lean4

instance [HasExplicitPullbacksOfInclusions P] : FinitaryExtensive (CompHausLike P) :=
  finitaryExtensive_of_preserves_and_reflects (compHausLikeToTop P)

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