English
If u is reachable to v in G and H is a subgraph of G that mirrors adjacency along its verts, and u is in H, then v is also in H.
Русский
Если из u можно дойти до v в G, и H — подграф G, который сохраняет смежность на вершинах H.verts, и u принадлежит H, то и v принадлежит H.
LaTeX
$$$\forall {u v} {H : G.Subgraph},\; G.Reachable u v \to (\forall v \in H.verts, \forall w, G.Adj v w \to H.Adj v w) \\to (u \in H.verts) \Rightarrow v \in H.verts.$$$
Lean4
theorem mem_subgraphVerts {u v} {H : G.Subgraph} (hr : G.Reachable u v) (h : ∀ v ∈ H.verts, ∀ w, G.Adj v w → H.Adj v w)
(hu : u ∈ H.verts) : v ∈ H.verts :=
by
let rec aux {v' : V} (hv' : v' ∈ H.verts) (p : G.Walk v' v) : v ∈ H.verts :=
by
by_cases hnp : p.Nil
· exact hnp.eq ▸ hv'
exact aux (H.edge_vert (h _ hv' _ (Walk.adj_snd hnp)).symm) p.tail
termination_by p.length
decreasing_by {
rw [← Walk.length_tail_add_one hnp]
omega
}
exact aux hu hr.some
