Edge cuts and bridges of graphs

This file defines the edge cuts and bridges of a graph.

Main definitions

• IsEdgeCut: a set of edges between a set of vertices and its complement.
• IsBridge: an edge that forms a singleton edge cut (an isthmus / bridge edge).
• IsBond: a bond of a graph is a minimal nonempty edge cut.

Edge cuts

def Graph.edgeCut {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) : Set β

The edge cut of a graph G along a set of vertices S.

Equations

• G.edgeCut S = {e : β | ∃ (u : α) (v : α), G.IsLink e u v ∧ u ∈ S ∧ v ∉ S}

theorem Graph.mem_edgeCut_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} {e : β} : e ∈ G.edgeCut S ↔ ∃ (u : α) (v : α), G.IsLink e u v ∧ u ∈ S ∧ v ∉ S

theorem Graph.IsLink.mem_edgeCut_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} {e : β} {u v : α} (h : G.IsLink e u v) : e ∈ G.edgeCut S ↔ u ∈ S ∧ v ∉ S ∨ v ∈ S ∧ u ∉ S

theorem Graph.edgeCut_subset_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} : G.edgeCut S ⊆ G.edgeSet

theorem Graph.edgeCut_eq_empty_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (hS : S ⊆ G.vertexSet) : G.edgeCut S = ∅ ↔ (G.induce S).IsClosedSubgraph G

@[simp]

theorem Graph.edgeCut_vertexSet_diff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} : G.edgeCut (G.vertexSet \ S) = G.edgeCut S

theorem Graph.IsSubgraph.edgeCut_eq_inter {α : Type u_1} {β : Type u_2} {G H : Graph α β} {S : Set α} (hHG : H ≤ G) : H.edgeCut S = H.edgeSet ∩ G.edgeCut S

@[simp]

theorem Graph.edgeCut_symmDiff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S S' : Set α} : G.edgeCut (symmDiff S S') = symmDiff (G.edgeCut S) (G.edgeCut S')

theorem Graph.IsClosedSubgraph.edgeCut_subset_edgeSet {α : Type u_1} {β : Type u_2} {G H : Graph α β} {S : Set α} (hHG : H.IsClosedSubgraph G) (hS : S ⊆ H.vertexSet) : G.edgeCut S ⊆ H.edgeSet

def Graph.IsEdgeCut {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : Prop

A set of edges is an edge cut if there exists a set of vertices such that the edges in the set are between the set of vertices and its complement.

Equations

• G.IsEdgeCut F = ∃ (S : Set α), G.edgeCut S = F

theorem Graph.IsEdgeCut.exists_edgeCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : G.IsEdgeCut F) : ∃ S ⊆ G.vertexSet, G.edgeCut S = F

theorem Graph.IsEdgeCut.exists_of_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {e : β} {u v : α} (he : G.IsLink e u v) (heF : e ∈ F) (hF : G.IsEdgeCut F) : ∃ S ⊆ G.vertexSet, G.edgeCut S = F ∧ u ∈ S ∧ v ∉ S

theorem Graph.IsEdgeCut.subset_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : G.IsEdgeCut F) : F ⊆ G.edgeSet

theorem Graph.IsEdgeCut.symmDiff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F F' : Set β} (hF : G.IsEdgeCut F) (hF' : G.IsEdgeCut F') : G.IsEdgeCut (symmDiff F F')

theorem Graph.IsEdgeCut.right_of_symmDiff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F F' : Set β} (hF : G.IsEdgeCut F) (hsymmDiff : G.IsEdgeCut (symmDiff F F')) : G.IsEdgeCut F'

theorem Graph.IsEdgeCut.left_of_symmDiff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F F' : Set β} (hF' : G.IsEdgeCut F') (hsymmDiff : G.IsEdgeCut (symmDiff F F')) : G.IsEdgeCut F

theorem Graph.IsEdgeCut.inter_edgeSet_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (hHG : H ≤ G) (hF : G.IsEdgeCut F) : H.IsEdgeCut (H.edgeSet ∩ F)

theorem Graph.IsEdgeCut.anti_of_subset {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (hHG : H ≤ G) (hFH : F ⊆ H.edgeSet) (hF : G.IsEdgeCut F) : H.IsEdgeCut F

theorem Graph.IsEdgeCut.of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (hGH : G.IsClosedSubgraph H) (hF : G.IsEdgeCut F) : H.IsEdgeCut F

theorem Graph.IsClosedSubgraph.isEdgeCut {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (hGH : G.IsClosedSubgraph H) (hF : G.IsEdgeCut F) : H.IsEdgeCut F

Alias of Graph.IsEdgeCut.of_isClosedSubgraph.

Bridges: singleton edge cuts

def Graph.IsBridge {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : Prop

A bridge (isthmus) is an edge that constitutes a singleton edge cut.

Equations

• G.IsBridge e = G.IsEdgeCut {e}

theorem Graph.IsBridge.isEdgeCut_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : G.IsBridge e) : G.IsEdgeCut {e}

theorem Graph.IsBridge.mem_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : G.IsBridge e) : e ∈ G.edgeSet

theorem Graph.IsBridge.anti_of_mem {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} (hHG : H ≤ G) (heH : e ∈ H.edgeSet) (he : G.IsBridge e) : H.IsBridge e

theorem Graph.IsBridge.of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} (hcle : H.IsClosedSubgraph G) (he : H.IsBridge e) : G.IsBridge e

theorem Graph.IsClosedSubgraph.isBridge_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} (he : e ∈ H.edgeSet) (h : H.IsClosedSubgraph G) : G.IsBridge e ↔ H.IsBridge e

Bonds: minimal nonempty edge cuts

def Graph.IsBond {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : Prop

A bond of a graph is a minimal nonempty edge-cut; see [Diestel, Graph Theory, Section 1.9][diestel2017].

Equations

• G.IsBond F = Minimal (fun (F : Set β) => G.IsEdgeCut F ∧ F.Nonempty) F

theorem Graph.IsBond.isEdgeCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {B : Set β} (hB : G.IsBond B) : G.IsEdgeCut B

theorem Graph.IsBond.nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {B : Set β} (hB : G.IsBond B) : B.Nonempty

theorem Graph.IsBond.subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {B : Set β} (hB : G.IsBond B) : B ⊆ G.edgeSet

theorem Graph.isBond_singleton_iff_isBridge {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} : G.IsBond {e} ↔ G.IsBridge e

theorem Graph.IsBridge.isBond_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} : G.IsBridge e → G.IsBond {e}

Alias of the reverse direction of Graph.isBond_singleton_iff_isBridge.

theorem Graph.IsBond.isBridge_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {B : Set β} {e : β} (heB : e ∈ B) (hB : G.IsBond B) : (G.deleteEdges (B \ {e})).IsBridge e

theorem Graph.IsBond.of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {B : Set β} (hGH : G.IsClosedSubgraph H) (hB : G.IsBond B) : H.IsBond B

theorem Graph.IsClosedSubgraph.isBond {α : Type u_1} {β : Type u_2} {G H : Graph α β} {B : Set β} (hGH : G.IsClosedSubgraph H) (hB : G.IsBond B) : H.IsBond B

Alias of Graph.IsBond.of_isClosedSubgraph.