IsSubwalk — Mathlib

English

Any walk is a subwalk of itself via the trivial subwalk data.

Русский

Любой обход является подпоследовательностью самого себя.

LaTeX

$$p.IsSubwalk p$$

Lean4

/-- `p.IsSubwalk q` means that the walk `p` is a contiguous subwalk of the walk `q`. -/
def IsSubwalk {u₁ v₁ u₂ v₂} (p : G.Walk u₁ v₁) (q : G.Walk u₂ v₂) : Prop :=
  ∃ (ru : G.Walk u₂ u₁) (rv : G.Walk v₁ v₂), q = (ru.append p).append rv

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