instMonoInl

Mathlib.CategoryTheory.Extensive

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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