The two sides of an edge

For a simple graph G and vertices u, v, the side G.edgeSide u v is the finite set of vertices still reachable from u after deleting the edge s(u, v). Every vertex reachable from u in G lies on the side of u or on the side of v, and the two sides are disjoint exactly when s(u, v) is a bridge. In a tree, deleting an edge therefore splits the vertices into the two sides of that edge: its fundamental partition.

In an acyclic graph the unique path between two vertices uses an edge exactly when that edge separates them, so a path from a vertex on the side of u crosses s(u, v) exactly when it ends off that side. These are the facts used to read off minimum cuts from weighted trees.

The side of u can also be recognized without walks: in a preconnected graph it is the unique set containing u but not v that no other edge leaves (SimpleGraph.edgeSide_eq_of_forall_adj). This identifies the sides of a tree after local changes to its edges. In a tree, the bipartitions given by the sides of two edges never cross (SimpleGraph.IsTree.not_crosses_edgeSide), so the edges of a tree determine a non-crossing family of cuts.

theorem SimpleGraph.Walk.IsPath.mem_edges_iff_not_reachable_deleteEdges {V : Type u_1} {G : SimpleGraph V} {s t : V} (hG : G.IsAcyclic) {p : G.Walk s t} (hp : p.IsPath) {e : Sym2 V} : e ∈ p.edges ↔ ¬(G.deleteEdges {e}).Reachable s t

In an acyclic graph, a path uses an edge exactly when deleting that edge separates the endpoints of the path.

noncomputable def SimpleGraph.edgeSide {V : Type u_1} [Fintype V] (G : SimpleGraph V) (u v : V) : Finset V

The side of u for the edge s(u, v): the vertices still reachable from u after deleting that edge. For a tree edge, G.edgeSide u v and G.edgeSide v u partition the vertices.

@[simp]

theorem SimpleGraph.mem_edgeSide {V : Type u_1} {G : SimpleGraph V} {u v x : V} [Fintype V] : x ∈ G.edgeSide u v ↔ (G.deleteEdges {s(u, v)}).Reachable u x

A vertex is on the side of u exactly when it is reachable from u without s(u, v).

theorem SimpleGraph.coe_edgeSide {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] : ↑(G.edgeSide u v) = ((G.deleteEdges {s(u, v)}).connectedComponentMk u).supp

The side of u is the vertex set of the connected component of u after deleting s(u, v).

theorem SimpleGraph.self_mem_edgeSide {V : Type u_1} [Fintype V] (G : SimpleGraph V) (u v : V) : u ∈ G.edgeSide u v

Each end of an edge lies on its own side.

theorem SimpleGraph.edgeSide_eq_singleton {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] (h : ∀ (y : V), G.Adj u y → y = v) : G.edgeSide u v = {u}

A vertex whose only neighbour is v is alone on its side of the edge to v.

theorem SimpleGraph.notMem_edgeSide_iff {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] : v ∉ G.edgeSide u v ↔ G.IsBridge s(u, v)

The far end of an edge is off the near side exactly when the edge is a bridge.

theorem SimpleGraph.IsBridge.notMem_edgeSide {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] (h : G.IsBridge s(u, v)) : v ∉ G.edgeSide u v

The far end of a bridge is not on the near side.

theorem SimpleGraph.reachable_deleteEdges_of_mem_edgeSide {V : Type u_1} {G : SimpleGraph V} {u v x : V} [Fintype V] {y : V} (hx : x ∈ G.edgeSide u v) (hy : y ∈ G.edgeSide u v) : (G.deleteEdges {s(u, v)}).Reachable x y

Two vertices on a common side of s(u, v) remain reachable after deleting it.

theorem SimpleGraph.Reachable.mem_edgeSide_or_mem_edgeSide {V : Type u_1} {G : SimpleGraph V} {u v x : V} [Fintype V] (h : G.Reachable u x) : x ∈ G.edgeSide u v ∨ x ∈ G.edgeSide v u

Every vertex reachable from u lies on the side of u or the side of v for s(u, v).

theorem SimpleGraph.IsBridge.disjoint_edgeSide {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] (h : G.IsBridge s(u, v)) : Disjoint (G.edgeSide u v) (G.edgeSide v u)

The two sides of a bridge are disjoint.

theorem SimpleGraph.IsBridge.compl_edgeSide {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] [DecidableEq V] (hG : G.Preconnected) (h : G.IsBridge s(u, v)) : (G.edgeSide u v)ᶜ = G.edgeSide v u

In a preconnected graph, the side of v for a bridge s(u, v) is the complement of the side of u.

theorem SimpleGraph.Adj.mem_edgeSide_iff {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] {y z : V} (h : G.Adj y z) (he : s(y, z) ≠ s(u, v)) : y ∈ G.edgeSide u v ↔ z ∈ G.edgeSide u v

An edge other than s(u, v) has both of its ends on the side of u, or neither.

theorem SimpleGraph.Adj.mem_edgeSide_iff_of_ne {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] {y z : V} (h : G.Adj y z) (hy : y ≠ v) (hz : z ≠ v) : y ∈ G.edgeSide u v ↔ z ∈ G.edgeSide u v

An edge whose ends both differ from v has both ends on the side of u for s(u, v), or neither.

theorem SimpleGraph.edgeSide_subset {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] {S : Finset V} (hu : u ∈ S) (hS : ∀ ⦃y z : V⦄, G.Adj y z → s(y, z) ≠ s(u, v) → y ∈ S → z ∈ S) : G.edgeSide u v ⊆ S

The side of u for s(u, v) is contained in every set that contains u and that no edge other than s(u, v) leaves.

theorem SimpleGraph.edgeSide_eq_of_forall_adj {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] (hG : G.Preconnected) {S : Finset V} (hu : u ∈ S) (hv : v ∉ S) (hS : ∀ ⦃y z : V⦄, G.Adj y z → s(y, z) ≠ s(u, v) → (y ∈ S ↔ z ∈ S)) : G.edgeSide u v = S

In a preconnected graph, a set containing u but not v, such that no edge other than s(u, v) has exactly one end in it, is the side of u for s(u, v).

theorem SimpleGraph.IsBridge.notMem_edgeSide_of_adj {V : Type u_1} {G : SimpleGraph V} [Fintype V] {r y z : V} (h : G.IsBridge s(y, r)) (hz : G.Adj r z) (hzy : z ≠ y) : z ∉ G.edgeSide y r

If s(y, r) is a bridge, every other neighbour of r lies off the side of y.

theorem SimpleGraph.Reachable.exists_adj_mem_edgeSide {V : Type u_1} {G : SimpleGraph V} [Fintype V] {r z : V} (h : G.Reachable r z) (hz : z ≠ r) : ∃ (y : V), G.Adj r y ∧ z ∈ G.edgeSide y r

Every vertex z ≠ r reachable from r lies on the side of some neighbour y of r for the edge s(y, r).

theorem SimpleGraph.IsTree.not_crosses_edgeSide {V : Type u_1} {G : SimpleGraph V} [Fintype V] (hG : G.IsTree) {a b c d : V} (hab : G.Adj a b) (hcd : G.Adj c d) : ¬(G.edgeSide a b).Crosses (G.edgeSide c d)

In a tree, the sides of two edges never cross: the bipartitions obtained by deleting tree edges form a non-crossing family.

theorem SimpleGraph.Walk.IsPath.mem_edges_iff_notMem_edgeSide {V : Type u_1} {G : SimpleGraph V} {u v : V} [Fintype V] {s t : V} (hG : G.IsAcyclic) {p : G.Walk s t} (hp : p.IsPath) (hs : s ∈ G.edgeSide u v) : s(u, v) ∈ p.edges ↔ t ∉ G.edgeSide u v

In an acyclic graph, a path starting on the side of u uses the edge s(u, v) exactly when it ends off that side.