nil_isSubwalk_iff_exists — Mathlib

English

For any q, nil is a subwalk of q iff q can be written as ru.append rv for some ru and rv.

Русский

Пусть q — обход. Тогда nil является подпрохождением q тогда и только тогда, когда q распадается на последовательность ru, rv, таких что q = ru.append rv.

LaTeX

$$$\forall G\;\forall q:G.Walk\,v\,w:\ IsSubwalk(nil:\, G.Walk\,v\,w) \iff \exists ru:G.Walk\,v\,u\,\exists rv:G.Walk\,u\,w, q = ru.append rv.$$$

Lean4

theorem nil_isSubwalk_iff_exists {u' u v} (q : G.Walk u v) :
    (Walk.nil : G.Walk u' u').IsSubwalk q ↔ ∃ (ru : G.Walk u u') (rv : G.Walk u' v), q = ru.append rv := by
  simp [IsSubwalk]

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