nil

Mathlib.Combinatorics.SimpleGraph.Paths

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

English

The empty walk from u to u is a path.

Русский

Пустой обход от u к u является путём.

LaTeX

$$$ (\mathrm{nil} : G.Walk u u).IsPath $$$

Lean4

theorem nil {u : V} : (nil : G.Walk u u).IsPath := by constructor <;> simp

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

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

Разделы

Аффилиация

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