pathEquivList_nil

Mathlib.Combinatorics.Quiver.SingleObj

URI: https://scilib.ai/kg/mathlib#Quiver.SingleObj.pathEquivList_nil

English

The equivalence pathEquivList sends the nil path to the empty list.

Русский

Биекция pathEquivList отправляет нулевой путь в пустой список.

LaTeX

$$$ \\text{pathEquivList\\_nil} : \\mathrm{pathEquivList}(\\mathrm{Path.nil}) = (\\,[]\\, : \\mathrm{List}(\\alpha)) $$$

Lean4

@[simp]
theorem pathEquivList_nil : pathEquivList Path.nil = ([] : List α) :=
  rfl

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

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

Разделы

Аффилиация

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