isSubwalk_nil_iff — Mathlib

English

For any q, p.IsSubwalk(nil) holds iff p has a representation nil.copy hu hv for some hu hv, i.e. p is the trivial walk up to endpoints.

Русский

Для любого q, p.IsSubwalk(nil) выполняется тогда и только тогда, когда p может быть записан как копия нуля с подходящими концами, то есть p — тривиальный обход до концов.

LaTeX

$$$\forall G\;\forall p:G.Walk\,u\,v:\ IsSubwalk(p, nil) \iff \exists hu: u'=u, hv: u'=v, p = nil.copy hu hv.$$$

Lean4

theorem isSubwalk_nil_iff {u v u'} (p : G.Walk u v) :
    p.IsSubwalk (nil : G.Walk u' u') ↔ ∃ (hu : u' = u) (hv : u' = v), p = nil.copy hu hv := by
  cases p with
  | nil =>
    constructor
    · rintro ⟨_ | _, _, ⟨⟩⟩
      simp
    · rintro ⟨rfl, _, _⟩
      simp
  | cons h p =>
    constructor
    · rintro ⟨_ | _, _, h⟩ <;> simp at h
    · rintro ⟨rfl, rfl, ⟨⟩⟩

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