inr_desc

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

URI: https://scilib.ai/kg/mathlib#CochainComplex.mappingCone.inr_desc

English

(inr φ) ≫ desc φ α β eq = β.

Русский

Пусть (inr φ) затем desc φ α β eq равны β.

LaTeX

$$$ (\mathrm{inr}(\phi)) \circ \desc(\phi, \alpha, \beta, eq) = β $$$

Lean4

@[reassoc (attr := simp)]
theorem inr_desc : inr φ ≫ desc φ α β eq = β := by cat_disch

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

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

Разделы

Аффилиация

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