instMonoι

Mathlib.CategoryTheory.Extensive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instMonoι

← MathLib Explorer

English

There is a canonical instance that makes Sigma.ι into monos for finite index families.

Русский

Существует канонический инстанс, делающий Sigma.ι монодля конечно индекса.

LaTeX

$$Instance: Mono( Sigma.ι )$$

Lean4

instance [FinitaryExtensive C] {ι : Type*} [Finite ι] (X : ι → C) (i : ι) : Mono (Sigma.ι X i) :=
  FinitaryExtensive.mono_ι (coproductIsCoproduct _) ⟨i⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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