exists_cons_eq_concat — Mathlib

English

For any p : G.Walk u v and h : G.Adj v w, there exist x, h' : G.Adj u x and q : G.Walk x w such that p.concat h = cons h' q.

Русский

Для любого p : G.Walk u v и h : G.Adj v w существуют x, h' : G.Adj u x и q : G.Walk x w такие, что p.concat h = cons h' q.

LaTeX

$$$$\forall {u,v,w} (p : G.Walk u v)(h : G.Adj v w),\ ∃ x\, ∃ h' : G.Adj u x\, ∃ q : G.Walk x w,\ p.concat h = cons h' q.$$$$

Lean4

/-- A non-trivial `cons` walk is representable as a `concat` walk. -/
theorem exists_cons_eq_concat {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
    ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w), cons h p = q.concat h' := by
  induction p generalizing u with
  | nil => exact ⟨_, nil, h, rfl⟩
  | cons h' p ih =>
    obtain ⟨y, q, h'', hc⟩ := ih h'
    refine ⟨y, cons h q, h'', ?_⟩
    rw [concat_cons, hc]

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