cons_isPath_iff — Mathlib

English

Appending an adjacent edge to a path yields a path iff the original path is a path and the start vertex is not used in the path.

Русский

Добавление смежного ребра к пути приводит к пути тогда и только тогда, когда исходный путь является путём и вершина-начало не встречается в пути.

LaTeX

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

Lean4

@[simp]
theorem cons_isPath_iff {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support :=
  by constructor <;> simp +contextual [isPath_def]

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