bicone_ι_π_ne

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.bicone_ι_π_ne

← MathLib Explorer

English

If j ≠ j', then the composition ι_j followed by π_{j'} is zero.

Русский

Если j ≠ j', то композиция ι_j;π_{j'} равна нулю.

LaTeX

$$$$ B.ι_j \\circ B.π_{j'} = 0 \\quad\\text{for } j \\neq j'. $$$$

Lean4

@[reassoc (attr := simp)]
theorem bicone_ι_π_ne {F : J → C} (B : Bicone F) {j j' : J} (h : j ≠ j') : B.ι j ≫ B.π j' = 0 := by
  simpa [h] using B.ι_π j j'

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

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

Разделы

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

Аффилиация

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