mem_support_of_mem_walk_support — Mathlib

English

If p is a nonempty walk, then every vertex appearing on p is in the graph's support.

Русский

Если p — непустой ход, то каждая вершина, встречающаяся на p, принадлежит поддержке графа.

LaTeX

$$$\forall G\,\forall u\forall v\ (p : G.Walk u v) (hp : \neg p.Nil) \Rightarrow \forall w \ (w \in p.support) \Rightarrow w \in G.support$$$

Lean4

theorem mem_support_of_mem_walk_support {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : ¬p.Nil) {w : V}
    (hw : w ∈ p.support) : w ∈ G.support :=
  by
  obtain ⟨y, hy⟩ := adj_of_mem_walk_support p hp hw
  exact (mem_support G).mpr ⟨y, hy.right⟩

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