preservesPullbackInr

Mathlib.CategoryTheory.Extensive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr

English

If C is small and locally small, then Arrow(C) is small.

Русский

Если C малая и локально-малая, то Arrow(C) малая.

LaTeX

$$$\text{Small}(\text{Arrow}(C))$$$

Lean4

noncomputable instance preservesPullbackInr : PreservesLimit (cospan coprod.inr f) F :=
  preservesPullback_symmetry _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru