of_cons

Mathlib.Combinatorics.SimpleGraph.Paths

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

English

If (cons h p) is a trail, then p is a trail whenever h is an adjacency in G.

Русский

Если (cons h p) является трайлом, то p тоже трайл, если h — смежность ребра в G.

LaTeX

$$of_cons : ∀ {u v w} {h : G.Adj u v} {p : G.Walk v w}, (cons h p).IsTrail → p.IsTrail$$

Lean4

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

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

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

Разделы

Аффилиация

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