shape

Mathlib.Algebra.Homology.HomotopyCofiber

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.homotopyCofiber.shape

English

For all i, j with hij, the equation inlX φ j i hij ∘ d φ i j equals φ.f j ∘ inrX φ j.

Русский

Для всех i, j с hij верно inlX φ j i hij ∘ d φ i j = φ.f j ∘ inrX φ j.

LaTeX

$$$ inlX\\,\\phi\\,j\\,i\\,hij \\circ d\\,φ\\,i\\,j = φ.f\\,j \\circ inrX\\,φ\\,j. $$$

Lean4

theorem shape (i j : ι) (hij : ¬c.Rel i j) : d φ i j = 0 :=
  dif_neg hij

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

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

Разделы

Аффилиация

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