exactAt_iff'

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.exactAt_iff'

← MathLib Explorer

English

For fixed i, j, k with hi hk, K.ExactAt j is equivalent to (K.sc' i j k).Exact.

Русский

Для фиксированных i, j, k с условиями hi hk, K.ExactAt j эквивалентно (K.sc' i j k).Exact.

LaTeX

$$$$ K.ExactAt(j) \iff (K.sc'(i,j,k)).Exact $$$$

Lean4

theorem exactAt_iff' (hi : c.prev j = i) (hk : c.next j = k) : K.ExactAt j ↔ (K.sc' i j k).Exact :=
  ShortComplex.exact_iff_of_iso (K.isoSc' i j k hi hk)

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

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

Разделы

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

Аффилиация

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