Walks and edge cuts

This file relates Mathlib's edge cuts Graph.edgeCut to edge-labelled multigraph walks. A walk that starts inside a vertex set and ends outside it traverses an edge of the cut, so a vertex set is closed under reachability exactly when its edge cut is empty. In particular, the set of vertices reachable from a point has empty edge cut, and every vertex set separating two mutually reachable vertices has a nonempty edge cut. Deleting edges removes them from every edge cut, and loops never cross a cut. In a graph on two distinct vertices, the edge cut of either vertex consists of all edges. An actual edge crosses a cut exactly when its unordered pair of ends crosses the corresponding set of actual vertices.

If the edge cut of T is contained in that of S, then the subgraph induced on S has empty edge cut along T; conversely when T ⊆ S.

These facts are the interface between cut-based and walk-based descriptions of connectivity, used for instance to characterize bridges by deletion.

For a simple graph, an edge of Graph.ofSimpleGraph G crosses a vertex set exactly when the corresponding unordered pair crosses it.

Implementation notes

Mathlib does not expose the body of Graph.IsEdgeCut and provides only elimination lemmas for it, so no edge cut can be produced outside its defining module. Graph.isEdgeCut_iff supplies the missing characterization; its proof unfolds the definition through import all.

theorem Graph.isEdgeCut_iff {α : Type u} {β : Type v} {G : Graph α β} {F : Set β} : G.IsEdgeCut F ↔ ∃ (S : Set α), G.edgeCut S = F

A set of edges is an edge cut exactly when it is the edge cut of some vertex set.

@[simp]

theorem Graph.isEdgeCut_edgeCut {α : Type u} {β : Type v} (G : Graph α β) (S : Set α) : G.IsEdgeCut (G.edgeCut S)

The edge cut of a vertex set is an edge cut.

@[simp]

theorem Graph.edgeCut_deleteEdges {α : Type u} {β : Type v} (G : Graph α β) (F : Set β) (S : Set α) : (G.deleteEdges F).edgeCut S = G.edgeCut S \ F

Deleting a set of edges removes exactly those edges from every edge cut.

theorem Graph.IsLoopAt.notMem_edgeCut {α : Type u} {β : Type v} {G : Graph α β} {S : Set α} {e : β} {x : α} (h : G.IsLoopAt e x) : e ∉ G.edgeCut S

A loop never crosses an edge cut.

theorem Graph.edgeEnds_crosses_iff_mem_edgeCut {α : Type u} {β : Type v} (G : Graph α β) (e : ↑G.edgeSet) (S : Set ↑G.vertexSet) : (G.edgeEnds e).Crosses S ↔ ↑e ∈ G.edgeCut (Subtype.val '' S)

An actual edge crosses a vertex cut exactly when its unordered pair of ends crosses the corresponding cut of actual vertices.

theorem Graph.Walk.exists_mem_edges_mem_edgeCut {α : Type u} {β : Type v} {G : Graph α β} {S : Set α} {x y : α} (p : G.Walk x y) (hx : x ∈ S) (hy : y ∉ S) : ∃ e ∈ p.edges, e ∈ G.edgeCut S

A walk from a vertex inside S to a point outside S traverses an edge of the edge cut of S.

theorem Graph.edgeCut_eq_empty_iff_forall_reachable {α : Type u} {β : Type v} {G : Graph α β} {S : Set α} : G.edgeCut S = ∅ ↔ ∀ ⦃x y : α⦄, G.Reachable x y → x ∈ S → y ∈ S

A vertex set has empty edge cut exactly when it is closed under reachability.

theorem Graph.Reachable.mem_of_edgeCut_eq_empty {α : Type u} {β : Type v} {G : Graph α β} {S : Set α} {x y : α} (h : G.Reachable x y) (hS : G.edgeCut S = ∅) (hx : x ∈ S) : y ∈ S

Reachability does not leave a vertex set with empty edge cut.

@[simp]

theorem Graph.edgeCut_setOf_reachable {α : Type u} {β : Type v} (G : Graph α β) (x : α) : G.edgeCut {y : α | G.Reachable x y} = ∅

The set of points reachable from a fixed point has empty edge cut.

theorem Graph.edgeCut_setOf_reachable_deleteEdges_subset {α : Type u} {β : Type v} (G : Graph α β) (F : Set β) (x : α) : G.edgeCut {y : α | (G.deleteEdges F).Reachable x y} ⊆ F

The boundary of the vertices reachable from x after deleting F is contained in F. Thus every edge separator contains an edge cut separating the same vertices.

theorem Graph.not_reachable_deleteEdges_edgeCut {α : Type u} {β : Type v} {S : Set α} {x y : α} (G : Graph α β) (hx : x ∈ S) (hy : y ∉ S) : ¬(G.deleteEdges (G.edgeCut S)).Reachable x y

Deleting every edge crossing a set leaves no path from inside the set to outside it.

theorem Graph.Reachable.edgeCut_nonempty {α : Type u} {β : Type v} {G : Graph α β} {S : Set α} {x y : α} (h : G.Reachable x y) (hxS : x ∈ S) (hyS : y ∉ S) : (G.edgeCut S).Nonempty

A vertex set containing one end of a reachable pair and missing the other has a nonempty edge cut.

@[simp]

theorem Graph.edgeCut_banana_singleton {α : Type u} {β : Type v} {u w : α} (huw : u ≠ w) (F : Set β) : (banana u w F).edgeCut {u} = F

The edge cut separating the two ends of a graph on two distinct vertices consists of all its edges.

Edge cuts of induced subgraphs

theorem Graph.edgeCut_induce_eq_empty_of_edgeCut_subset {α : Type u} {β : Type v} {G : Graph α β} {S T : Set α} (h : G.edgeCut T ⊆ G.edgeCut S) : (G.induce S).edgeCut T = ∅

If every edge crossing T also crosses S, then no edge with both ends in S crosses T: the subgraph induced on S has empty edge cut along T.

theorem Graph.edgeCut_subset_edgeCut_of_edgeCut_induce_eq_empty {α : Type u} {β : Type v} {G : Graph α β} {S T : Set α} (hTS : T ⊆ S) (h : (G.induce S).edgeCut T = ∅) : G.edgeCut T ⊆ G.edgeCut S

If T ⊆ S has empty edge cut in the subgraph induced on S, then every edge crossing T also crosses S.

theorem SimpleGraph.mem_edgeCut_ofSimpleGraph_iff_crosses {V : Type u} {G : SimpleGraph V} {e : Sym2 V} {S : Set V} (he : e ∈ G.edgeSet) : e ∈ (Graph.ofSimpleGraph G).edgeCut S ↔ e.Crosses S

An edge of Graph.ofSimpleGraph G belongs to the edge cut of S exactly when its unordered pair of endpoints crosses S.