pathStar

Mathlib.Combinatorics.Quiver.Covering

URI: https://scilib.ai/kg/mathlib#Prefunctor.pathStar

Lean4

/-- A prefunctor induces a map of path stars. -/
def pathStar (u : U) : Quiver.PathStar u → Quiver.PathStar (φ.obj u) := fun p => Quiver.PathStar.mk (φ.mapPath p.2)

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

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

Разделы

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

Аффилиация

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