toSubgraph_adj_snd — Mathlib

English

If a nonempty walk w is considered, then the first edge in the walk is an edge in the subgraph from its start vertex.

Русский

Если обход непустой, первый ребром обхода является ребро подграфа, начинающегося в начальной вершине.

LaTeX

$${u v} (w : G.Walk u v) (h : ¬w.Nil) : w.toSubgraph.Adj u w.snd$$

Lean4

theorem toSubgraph_adj_snd {u v} (w : G.Walk u v) (h : ¬w.Nil) : w.toSubgraph.Adj u w.snd := by
  simpa using w.toSubgraph_adj_getVert (not_nil_iff_lt_length.mp h)

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