mem_support_of_adj_toSubgraph — Mathlib

English

If p.toSubgraph.Adj u' v' holds, then u' is in the support of p.

Русский

Если в подграфе обхода есть ребро между u' и v', то вершина u' принадлежит поддержке обхода.

LaTeX

$$$ p.toSubgraph.Adj u' v' \Rightarrow u' \in p.support $$$

Lean4

theorem mem_support_of_adj_toSubgraph {u v u' v' : V} {p : G.Walk u v} (hp : p.toSubgraph.Adj u' v') : u' ∈ p.support :=
  p.mem_verts_toSubgraph.mp (p.toSubgraph.edge_vert hp)

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