bypass_isPath — Mathlib

English

For any walk p, the bypass of p is a path.

Русский

Для любой обходной дорожки p конструированная операция обхода (bypass) дает путь.

LaTeX

$$$ \forall {V} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} (p : G.Walk u v), p.bypass.IsPath$$$

Lean4

theorem bypass_isPath {u v : V} (p : G.Walk u v) : p.bypass.IsPath := by
  induction p with
  | nil => simp!
  | cons _ p' ih =>
    simp only [bypass]
    split_ifs with hs
    · exact ih.dropUntil hs
    · simp [*, cons_isPath_iff]

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