isInitialSingleObjApply

Mathlib.CategoryTheory.GradedObject.Single

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GradedObject.isInitialSingleObjApply

Lean4

/-- The object `(single j).obj X i` is initial when `i ≠ j`. -/
noncomputable def isInitialSingleObjApply (j : J) (X : C) (i : J) (h : i ≠ j) : IsInitial ((single j).obj X i) :=
  by
  dsimp [single]
  rw [if_neg h]
  exact initialIsInitial

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

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

Разделы

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

Аффилиация

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