hasPullbackInr

Mathlib.CategoryTheory.Extensive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr

English

For F: C ⥤ D with HasBinaryCoproducts and HasPullbacksOfInclusions, the HasPullback along coprod.inr exists.

Русский

Для F: C → D с HasBinaryCoproducts и HasPullbacksOfInclusions существует вытянутый предел вдоль coprod.inr.

LaTeX

$$$\text{HasPullback } f\,\text{ coprod.inr}$$$

Lean4

instance hasPullbackInr : HasPullback coprod.inr f :=
  hasPullback_symmetry _ _

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

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

Разделы

Аффилиация

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