set_walk_length_succ_eq — Mathlib

English

Walks of length n+1 from u to v are obtained by choosing a neighbor w of u and appending a length-n walk from w to v.

Русский

Ходы длины n+1 от u к v получаются за счет выбора соседа w u и дополнения длины-n хода от w к v к началу.

LaTeX

$${p : G.Walk u v | p.length = n.succ} = ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' : G.Walk w v | p'.length = n}$$

Lean4

theorem set_walk_length_succ_eq (u v : V) (n : ℕ) :
    {p : G.Walk u v | p.length = n.succ} =
      ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' : G.Walk w v | p'.length = n} :=
  by
  ext p
  cases p with
  | nil => simp [eq_comm]
  | cons huw
    pwv =>
    simp only [Nat.succ_eq_add_one, Set.mem_setOf_eq, Walk.length_cons, add_left_inj, Set.mem_iUnion, Set.mem_image]
    grind

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