map_snd_darts

Mathlib.Combinatorics.SimpleGraph.Walk

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Walk.map_snd_darts

← MathLib Explorer

English

The list of second coordinates of all darts equals the tail of the walk's vertex support.

Русский

Список вторых координат всех дротиков равен хвосту списка вершин обхода.

LaTeX

$$$p.\\darts\\.map\\ (\\lambda x. x\\.snd) = p.\\support.\\tail$$$

Lean4

theorem map_snd_darts {u v : V} (p : G.Walk u v) : p.darts.map (·.snd) = p.support.tail := by
  simpa using congr_arg List.tail (cons_map_snd_darts p)

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

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

Разделы

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

Аффилиация

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