length_bypass_le — Mathlib

English

For any walk p, the length of its bypass is at most the length of p.

Русский

Для любой обходной дорожки p длина обхода меньше или равна длине самой дорожки.

LaTeX

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

Lean4

theorem length_bypass_le {u v : V} (p : G.Walk u v) : p.bypass.length ≤ p.length := by
  induction p with
  | nil => rfl
  | cons _ _ ih =>
    simp only [bypass]
    split_ifs
    · trans
      · apply length_dropUntil_le
      rw [length_cons]
      cutsat
    · rw [length_cons, length_cons]
      exact Nat.add_le_add_right ih 1

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