of_append_right

Mathlib.Combinatorics.SimpleGraph.Paths

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

← MathLib Explorer

English

If (p.append q) is a path, then q is a path.

Русский

Если объединение обходов p и q образуют путь, то путь q — путь.

LaTeX

$$$ (p.append q).IsPath \Rightarrow q.IsPath $$$

Lean4

theorem of_append_right {u v w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsPath) : q.IsPath :=
  by
  rw [← isPath_reverse_iff] at h ⊢
  rw [reverse_append] at h
  apply h.of_append_left

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

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

Разделы

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

Аффилиация

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