tarList

Mathlib.Tactic.Widget.StringDiagram

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Widget.StringDiagram.Node.tarList

Lean4

/-- The codomain of the 2-morphism associated with a node as a list
(the first component is the node itself). -/
def tarList : Node → List (Node × Atom₁)
  | Node.atom n => n.atom.tgt.toList.map (fun f ↦ (.atom n, f))
  | Node.id n => [(.id n, n.id)]

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

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

Разделы

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

Аффилиация

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