of_cons

Mathlib.Combinatorics.SimpleGraph.Paths

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

English

If the walk cons(h,p) is a path, then p is a path.

Русский

Если обход, образованный cons(h,p), является путём, то и сам p является путём.

LaTeX

$$$ (\mathrm{cons}(h,p)).IsPath \Rightarrow p.IsPath $$$

Lean4

theorem of_cons {u v w : V} {h : G.Adj u v} {p : G.Walk v w} : (cons h p).IsPath → p.IsPath := by simp [isPath_def]

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

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

Разделы

Аффилиация

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