pathEquivList — Mathlib

English

Paths in the single-object α quiver from star α to star α are in natural bijection with lists of elements of α; the bijection is given by mapping a path to its list of edge labels and back.

Русский

Пути в единичном объекте квира α от star α к star α находятся в естественной биекции со списками элементов α; биекция задаётся отображением пути в список ребер и обратно.

LaTeX

$$$ \\text{pathEquivList} : \\mathrm{Path}(\\mathrm{star}\\,\\alpha, \\mathrm{star}\\,\\alpha) \\ \\simeq\\ \\mathrm{List}(\\alpha) $$$

Lean4

/-- Paths in `SingleObj α` quiver correspond to lists of elements of type `α`. -/
def pathEquivList : Path (star α) (star α) ≃ List α :=
  ⟨pathToList, listToPath, fun p => listToPath_pathToList p, pathToList_listToPath⟩

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