of_adj

Mathlib.Combinatorics.SimpleGraph.Paths

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

English

The path corresponding to an adjacent edge is a path.

Русский

Путь, соответствующий смежному ребру, является путём.

LaTeX

$$$ h.toWalk.IsPath $$$

Lean4

theorem of_adj {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : h.toWalk.IsPath := by aesop

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

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

Разделы

Аффилиация

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