instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop

English

The functor to TopCat preserves pullbacks in the WalkingCospan, i.e., preserves limits of the shape cospan f g.

Русский

Функтор в TopCat сохраняет пулбэки в WalkingCospan, то есть сохраняет пределы в форме пула (f,g).

LaTeX

$$$\\text{PreservesLimit}(\\mathrm{cospan}\\ f\\ g)\\ (\\mathrm{CompHausLikeToTop}\\ P)$$$

Lean4

/-- The functor to `TopCat` preserves pullbacks. -/
noncomputable instance : PreservesLimit (cospan f g) (compHausLikeToTop P) :=
  preservesLimit_of_createsLimit_and_hasLimit _ _

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