isComplex₁

Mathlib.Algebra.Homology.ExactSequence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ComposableArrows.isComplex₁

English

For any S in ComposableArrows C 1, S is a complex.

Русский

Для любого S в ComposableArrows C 1S является комплексом.

LaTeX

$$$S \in \mathrm{ComposableArrows}(C,1) \implies S \text{ is a complex}$$$

Lean4

theorem isComplex₁ (S : ComposableArrows C 1) : S.IsComplex where zero i hi := by omega

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

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

Разделы

Аффилиация

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