stupidTruncMap_comp

Mathlib.Algebra.Homology.Embedding.StupidTrunc

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.stupidTruncMap_comp

← MathLib Explorer

English

Stupid truncation respects composition of morphisms.

Русский

Грубое усечение сохраняет композицию морфизмов.

LaTeX

$$$stupidTruncMap(\phi \circ \psi, e) = stupidTruncMap(\phi, e) \circ stupidTruncMap(\psi, e)$$$

Lean4

@[simp, reassoc]
theorem stupidTruncMap_comp : stupidTruncMap (φ ≫ φ') e = stupidTruncMap φ e ≫ stupidTruncMap φ' e := by
  simp [stupidTruncMap, stupidTrunc]

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

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

Разделы

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

Аффилиация

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