cons

Mathlib.Combinatorics.SimpleGraph.Paths

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

← MathLib Explorer

English

If p is a path and u is not in p, then cons(h,p) is a path.

Русский

Если p — путь, и вершина u не встречается в p, то cons(h,p) — путь.

LaTeX

$$$ p.IsPath \land u \notin p.support \Rightarrow (\mathrm{cons}(h,p)).IsPath $$$

Lean4

protected theorem cons {p : Walk G v w} (hp : p.IsPath) (hu : u ∉ p.support) {h : G.Adj u v} : (cons h p).IsPath :=
  (cons_isPath_iff _ _).2 ⟨hp, hu⟩

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

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

Разделы

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

Аффилиация

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