mem_iff

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.HomComplex.Cocycle.mem_iff

English

Cocycle is a subtype of Cochain: Cocycle(F,G,n) ⊆ Cochain(F,G,n) characterized by δ n (n+1) z = 0.

Русский

Cocycle является подвидами Cochain: Cocycle(F,G,n) ⊆ Cochain(F,G,n), задаётся условием δ n (n+1) z = 0.

LaTeX

$$Cocycle(F,G,n) = { z ∈ Cochain(F,G,n) : δ n (n+1) z = 0 }$$

Lean4

theorem mem_iff (hnm : n + 1 = m) (z : Cochain F G n) : z ∈ cocycle F G n ↔ δ n m z = 0 := by subst hnm; rfl

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

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

Разделы

Аффилиация

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