preservesPullbackInl'

Mathlib.CategoryTheory.Extensive

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

English

For a thin category, EssentiallySmall C is equivalent to Small(Skeleton C).

Русский

Для тонкой категории EssentiallySmall(C) эквивалентно Small(Skeleton(C)).

LaTeX

$$$\text{EssentiallySmall}(C) \iff \text{Small}(\text{Skeleton}(C))$$$

Lean4

noncomputable instance preservesPullbackInl' : PreservesLimit (cospan f coprod.inl) F :=
  preservesPullback_symmetry _ _ _

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

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

Разделы

Аффилиация

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