exactAt_of_isGE

Mathlib.Algebra.Homology.Embedding.CochainComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.exactAt_of_isGE

← MathLib Explorer

English

If K is GE at level n, then K is exact at all degrees i with i < n.

Русский

Если K ге по уровню n, то тождественная точка в каждом mėде i < n равна точной.

LaTeX

$$$\forall i

Lean4

theorem exactAt_of_isGE (n i : ℤ) (hi : i < n) [K.IsGE n] : K.ExactAt i :=
  exactAt_of_isSupported K (embeddingUpIntGE n) i (by simpa only [notMem_range_embeddingUpIntGE_iff] using hi)

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

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

Разделы

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

Аффилиация

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