SimpleGraph.Walk.IsEulerian.mem_edges_iff

theorem SimpleGraph.Walk.IsEulerian.mem_edges_iff : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v}, p.IsEulerian → ∀ {e : Sym2 V}, e ∈ p.edges ↔ e ∈ G.edgeSet

This theorem states that for any simple graph `G` with vertex set `V` (where `V` has decidable equality) and any vertices `u`, `v` in `V`, if `p` is an Eulerian walk from `u` to `v` in `G` (which means `p` is a walk that visits each edge of `G` exactly once), then for any edge `e` (represented as an unordered pair of vertices), `e` is an edge of the walk `p` if and only if `e` is an edge in the graph `G`. This captures the idea that an Eulerian walk precisely uses all the edges in the graph once.

More concisely: For any simple graph with decidable vertex equality and any two vertices, an Eulerian walk connects them if and only if the edges in the walk belong to the graph.