instMonoInr

Mathlib.CategoryTheory.Extensive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instMonoInr

English

Instance provides that for X,Y in a finitely extensive category, coprod.inr is mono.

Русский

Экземпляр обеспечивает, что coprod.inr моно для X,Y в финитно-расширяемой категории.

LaTeX

$$$\text{Mono}(\text{coprod}.\text{inr})$$$

Lean4

instance [FinitaryExtensive C] (X Y : C) : Mono (coprod.inr : Y ⟶ X ⨿ Y) :=
  (FinitaryExtensive.mono_inr_of_isColimit (coprodIsCoprod X Y) :)

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

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

Разделы

Аффилиация

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