concat_isPath_iff — Mathlib

English

For a path p and an edge h, p.concat(h) is a path iff p is a path and the new vertex w is not in p's support.

Русский

Для пути p и ребра h, p.concat(h) является путём тогда и только тогда, когда p — путь и вершина w не входит в поддержку p.

LaTeX

$$$ (p.concat(h)).IsPath \iff p.IsPath \land w \notin p.support $$$

Lean4

theorem concat_isPath_iff {p : G.Walk u v} (h : G.Adj v w) : (p.concat h).IsPath ↔ p.IsPath ∧ w ∉ p.support :=
  by
  rw [← (p.concat h).isPath_reverse_iff, ← p.isPath_reverse_iff, reverse_concat, ← List.mem_reverse, ← support_reverse]
  exact cons_isPath_iff h.symm p.reverse

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