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

∫ Утверждение Mathlib

next

Mathlib.Algebra.Homology.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.Hom.next

← MathLib Explorer

Lean4

/-- `f.next i` is `f.f j` if there is some `r i j`, and `f.f j` otherwise. -/
abbrev next (f : Hom C₁ C₂) (i : ι) : C₁.xNext i ⟶ C₂.xNext i :=
  f.f _

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

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

Разделы

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

Аффилиация

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

© 2026 SciLib Lab · ФИЦ ИУ РАН. Все права защищены. Контакты: info@scilibai.ru