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

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

prev

Mathlib.Algebra.Homology.HomologicalComplex

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

← MathLib Explorer

Lean4

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

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

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

Разделы

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

Аффилиация

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

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