Sides of tree edges

For an edge uv of a graph T on a finite vertex type, SimpleGraph.edgeSide T u v is the set of vertices reachable from u once the edge uv is deleted. In a tree, the two sides of an edge partition the vertices, a path crosses each of its edges from one side to the other, and a set that no other tree edge crosses is a side. These are the fundamental cuts of a tree, used by Gomory–Hu trees (CslibFrontier.Algorithms.Lean.GomoryHu.Basic).

Main definitions

• SimpleGraph.edgeSide: the vertices reachable from u in T after deleting the edge uv.

Main results

• SimpleGraph.mem_edgeSide_swap, SimpleGraph.edgeSide_swap: in a tree, the two sides of an edge are complementary.
• SimpleGraph.mem_edgeSide_of_mem_darts: along a path in a forest, the start and the end of the path lie on opposite sides of each edge of the path.
• SimpleGraph.Reachable.mem_iff_of_forall_adj: if no edge other than uv crosses a set, then no path avoiding uv crosses it.
• SimpleGraph.edgeSide_eq_of_forall_adj: a set containing u, missing v and crossed by no other tree edge is the side of uv containing u.

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

The side of the edge uv containing u in a graph T: the vertices reachable from u once the edge s(u, v) is deleted. For an edge uv of a tree, this is the component of u in T - uv.

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

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

theorem SimpleGraph.notMem_edgeSide_of_isAcyclic {V : Type u_1} [Fintype V] {T : SimpleGraph V} (hT : T.IsAcyclic) {u v : V} (huv : T.Adj u v) : v ∉ T.edgeSide u v

theorem SimpleGraph.mem_edgeSide_swap {V : Type u_1} [Fintype V] {T : SimpleGraph V} (hT : T.IsTree) {u v : V} (huv : T.Adj u v) (x : V) : x ∈ T.edgeSide v u ↔ x ∉ T.edgeSide u v

In a tree, the two sides of an edge partition the vertices.

theorem SimpleGraph.edgeSide_swap {V : Type u_1} [Fintype V] {T : SimpleGraph V} [DecidableEq V] (hT : T.IsTree) {u v : V} (huv : T.Adj u v) : T.edgeSide v u = (T.edgeSide u v)ᶜ

In a tree, the side of vu containing v is the complement of the side of uv containing u.

theorem SimpleGraph.mem_edgeSide_of_mem_darts {V : Type u_1} [Fintype V] {T : SimpleGraph V} (hT : T.IsAcyclic) {s t : V} {p : T.Walk s t} (hp : p.IsPath) {d : T.Dart} (hd : d ∈ p.darts) : s ∈ T.edgeSide d.toProd.1 d.toProd.2 ∧ t ∉ T.edgeSide d.toProd.1 d.toProd.2

Along a path in a forest, the start and the end of the path lie on the two sides of each of its darts.

theorem SimpleGraph.Reachable.mem_iff_of_forall_adj {V : Type u_1} {T : SimpleGraph V} {u v x y : V} {S : Finset V} (h : (T.deleteEdges {s(u, v)}).Reachable x y) (hS : ∀ ⦃a b : V⦄, T.Adj a b → s(a, b) ≠ s(u, v) → (a ∈ S ↔ b ∈ S)) : x ∈ S ↔ y ∈ S

If no edge of T other than uv crosses S, then deleting uv leaves no path across S.

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

A criterion for the side of a tree edge: if S contains u, misses v, and no other edge of the tree T crosses S, then S is the side of uv containing u.