Edge reachability and edge connectivity of multigraphs

Two points x, y of a multigraph G : Graph α β are k-edge-reachable, G.IsEdgeReachable k x y, when they remain reachable after deleting any set of fewer than k edges, and G is k-edge-connected, G.IsEdgeConnected k, when any two of its actual vertices are k-edge-reachable. Deleted edges are counted as edge identities, so parallel edges count separately: two vertices joined by n parallel edges are n-edge-reachable. The thresholds are natural numbers, and G.edgeReachability x y and G.edgeConnectivity are the suprema in ℕ∞ of the thresholds at which the predicates hold. These supremum definitions and the bounds by incident edge counts follow mathlib4#42494.

The predicates follow Mathlib's SimpleGraph.IsEdgeReachable and SimpleGraph.IsEdgeConnected, and agree with them on Graph.ofSimpleGraph. Unlike a simple graph, a multigraph has actual vertices V(G) inside its ambient vertex type, and reachability requires actual endpoints. So for k ≠ 0 a point is k-edge-reachable from itself exactly when it is an actual vertex, and k-edge-reachability is an equivalence relation on V(G). Global edge connectivity only quantifies over actual vertices, so it is monotone along inclusions of multigraphs with the same actual vertex set.

Main results

• Graph.isEdgeReachable_one, Graph.isEdgeConnected_one: the threshold 1 is reachability.
• Graph.isEdgeConnected_iff_forall_connected: a multigraph with an actual vertex is k-edge-connected exactly when it stays connected after deleting fewer than k edges.
• Graph.IsLink.isBridge_iff_not_isEdgeReachable_two: an edge is a bridge exactly when its ends are not 2-edge-reachable.
• Graph.isEdgeConnected_two_iff_forall_reachable_and_forall_not_isBridge: a multigraph is 2-edge-connected exactly when its actual vertices are pairwise reachable and it has no bridge. Graph.forall_reachable_isEdgeReachable_two_iff_forall_not_isBridge is the componentwise form, and Graph.preconnected_and_forall_not_isBridge_ofSimpleGraph_iff compares the criterion on Graph.ofSimpleGraph with Mathlib's SimpleGraph.isEdgeConnected_two_iff_forall_not_isBridge.
• Graph.isEdgeReachable_ofSimpleGraph_iff, Graph.isEdgeConnected_ofSimpleGraph_iff: agreement with the simple-graph predicates.
• Graph.isEdgeReachable_iff_le_edgeReachability, Graph.isEdgeConnected_iff_le_edgeConnectivity: the numerical invariants record exactly the thresholds at which the predicates hold.
• Graph.edgeConnectivity_ofSimpleGraph: agreement with the simple-graph edge connectivity.
• Graph.edgeConnectivity_eq_iInf_edgeReachability: edge connectivity is the least local edge reachability between actual vertices.
• Graph.edgeReachability_le_nonloopIncidenceCount: local edge reachability between distinct vertices is bounded by the number of nonloop edges at the first vertex.
• Graph.edgeConnectivity_eq_top_iff: when the actual edge set is finite, edge connectivity is ⊤ exactly when there is at most one actual vertex.
• Graph.edgeReachability_banana, Graph.edgeConnectivity_banana: two distinct vertices joined by n parallel edges have local edge reachability and edge connectivity n.

Edge reachability

def Graph.IsEdgeReachable {α : Type u} {β : Type v} (G : Graph α β) (k : ℕ) (x y : α) : Prop

Two points of a multigraph are k-edge-reachable if they remain reachable after deleting any set of fewer than k edges.

theorem Graph.isEdgeReachable_def {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x y : α} : G.IsEdgeReachable k x y ↔ ∀ ⦃F : Set β⦄, F.encard < ↑k → (G.deleteEdges F).Reachable x y

theorem Graph.isEdgeReachable_iff_forall_subset_edgeSet {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x y : α} : G.IsEdgeReachable k x y ↔ ∀ ⦃F : Set β⦄, F ⊆ G.edgeSet → F.encard < ↑k → (G.deleteEdges F).Reachable x y

Only actual edges need to be deleted in the definition of edge reachability.

@[simp]

theorem Graph.IsEdgeReachable.zero {α : Type u} {β : Type v} {G : Graph α β} {x y : α} : G.IsEdgeReachable 0 x y

@[simp]

theorem Graph.isEdgeReachable_one {α : Type u} {β : Type v} {G : Graph α β} {x y : α} : G.IsEdgeReachable 1 x y ↔ G.Reachable x y

Reachability is 1-edge-reachability.

theorem Graph.IsEdgeReachable.anti {α : Type u} {β : Type v} {G : Graph α β} {k l : ℕ} {x y : α} (hkl : k ≤ l) (h : G.IsEdgeReachable l x y) : G.IsEdgeReachable k x y

Edge reachability at a smaller threshold follows from edge reachability at a larger one.

theorem Graph.IsEdgeReachable.mono {α : Type u} {β : Type v} {G H : Graph α β} {k : ℕ} {x y : α} (hGH : G ≤ H) (h : G.IsEdgeReachable k x y) : H.IsEdgeReachable k x y

Edge reachability is monotone under inclusion of multigraphs.

theorem Graph.IsEdgeReachable.reachable {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x y : α} (hk : k ≠ 0) (h : G.IsEdgeReachable k x y) : G.Reachable x y

theorem Graph.IsEdgeReachable.left_mem {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x y : α} (hk : k ≠ 0) (h : G.IsEdgeReachable k x y) : x ∈ G.vertexSet

theorem Graph.IsEdgeReachable.right_mem {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x y : α} (hk : k ≠ 0) (h : G.IsEdgeReachable k x y) : y ∈ G.vertexSet

theorem Graph.IsEdgeReachable.refl {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x : α} (hx : x ∈ G.vertexSet) : G.IsEdgeReachable k x x

An actual vertex is k-edge-reachable from itself, since deleting edges keeps every vertex.

theorem Graph.isEdgeReachable_self_iff {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x : α} (hk : k ≠ 0) : G.IsEdgeReachable k x x ↔ x ∈ G.vertexSet

For a positive threshold, a point is k-edge-reachable from itself exactly when it is an actual vertex.

theorem Graph.IsEdgeReachable.symm {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x y : α} (h : G.IsEdgeReachable k x y) : G.IsEdgeReachable k y x

theorem Graph.isEdgeReachable_comm {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x y : α} : G.IsEdgeReachable k x y ↔ G.IsEdgeReachable k y x

theorem Graph.IsEdgeReachable.trans {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x y z : α} (hxy : G.IsEdgeReachable k x y) (hyz : G.IsEdgeReachable k y z) : G.IsEdgeReachable k x z

theorem Graph.isEdgeReachable_equivalence {α : Type u} {β : Type v} (G : Graph α β) (k : ℕ) : Equivalence fun (x y : ↑G.vertexSet) => G.IsEdgeReachable k ↑x ↑y

For every threshold, edge reachability is an equivalence relation on the actual vertices.

Edge connectivity

def Graph.IsEdgeConnected {α : Type u} {β : Type v} (G : Graph α β) (k : ℕ) : Prop

A multigraph is k-edge-connected if any two of its actual vertices are k-edge-reachable.

theorem Graph.isEdgeConnected_def {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} : G.IsEdgeConnected k ↔ ∀ ⦃x : α⦄, x ∈ G.vertexSet → ∀ ⦃y : α⦄, y ∈ G.vertexSet → G.IsEdgeReachable k x y

theorem Graph.IsEdgeConnected.isEdgeReachable {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x y : α} (h : G.IsEdgeConnected k) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : G.IsEdgeReachable k x y

@[simp]

theorem Graph.IsEdgeConnected.zero {α : Type u} {β : Type v} {G : Graph α β} : G.IsEdgeConnected 0

@[simp]

theorem Graph.isEdgeConnected_one {α : Type u} {β : Type v} {G : Graph α β} : G.IsEdgeConnected 1 ↔ ∀ ⦃x : α⦄, x ∈ G.vertexSet → ∀ ⦃y : α⦄, y ∈ G.vertexSet → G.Reachable x y

A multigraph is 1-edge-connected exactly when any two actual vertices are reachable from each other.

theorem Graph.IsEdgeConnected.anti {α : Type u} {β : Type v} {G : Graph α β} {k l : ℕ} (hkl : k ≤ l) (h : G.IsEdgeConnected l) : G.IsEdgeConnected k

theorem Graph.IsEdgeConnected.mono {α : Type u} {β : Type v} {G H : Graph α β} {k : ℕ} (hGH : G ≤ H) (hV : G.vertexSet = H.vertexSet) (h : G.IsEdgeConnected k) : H.IsEdgeConnected k

Edge connectivity is monotone under inclusions of multigraphs with the same actual vertices. Without equal vertex sets this fails: the larger graph may have additional, isolated vertices.

theorem Graph.IsEdgeConnected.of_subsingleton {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} (hG : G.vertexSet.Subsingleton) : G.IsEdgeConnected k

A multigraph with at most one actual vertex is k-edge-connected for every k.

theorem Graph.IsEdgeConnected.connected {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} (hk : k ≠ 0) (hV : G.vertexSet.Nonempty) (h : G.IsEdgeConnected k) : G.Connected

A k-edge-connected multigraph with an actual vertex is connected, for k ≠ 0.

theorem Graph.isEdgeConnected_iff_forall_connected {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} (hV : G.vertexSet.Nonempty) : G.IsEdgeConnected k ↔ ∀ ⦃F : Set β⦄, F.encard < ↑k → (G.deleteEdges F).Connected

A multigraph with an actual vertex is k-edge-connected exactly when it remains connected after deleting any set of fewer than k edges.

Bridges

theorem Graph.IsBridge.not_isEdgeReachable_two {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y : α} (he : G.IsBridge e) (h : G.IsLink e x y) : ¬G.IsEdgeReachable 2 x y

The ends of a link of a bridge are not 2-edge-reachable.

theorem Graph.IsLink.isBridge_iff_not_isEdgeReachable_two {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y : α} (h : G.IsLink e x y) : G.IsBridge e ↔ ¬G.IsEdgeReachable 2 x y

An edge joining x and y is a bridge exactly when x and y are not 2-edge-reachable.

theorem Graph.Reachable.isEdgeReachable_two {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (h : ∀ (e : β), ¬G.IsBridge e) (hxy : G.Reachable x y) : G.IsEdgeReachable 2 x y

In a multigraph without bridges, any two vertices reachable from each other are 2-edge-reachable.

theorem Graph.forall_reachable_isEdgeReachable_two_iff_forall_not_isBridge {α : Type u} {β : Type v} {G : Graph α β} : (∀ ⦃x y : α⦄, G.Reachable x y → G.IsEdgeReachable 2 x y) ↔ ∀ (e : β), ¬G.IsBridge e

Any two vertices of a multigraph reachable from each other are 2-edge-reachable exactly when the multigraph has no bridge; that is, every connected component is 2-edge-connected exactly when there is no bridge.

theorem Graph.isEdgeConnected_two_iff_forall_reachable_and_forall_not_isBridge {α : Type u} {β : Type v} {G : Graph α β} : G.IsEdgeConnected 2 ↔ (∀ ⦃x : α⦄, x ∈ G.vertexSet → ∀ ⦃y : α⦄, y ∈ G.vertexSet → G.Reachable x y) ∧ ∀ (e : β), ¬G.IsBridge e

A multigraph is 2-edge-connected exactly when any two of its actual vertices are reachable from each other and it has no bridge. No finiteness is assumed; when there is no actual vertex, both sides hold.

theorem Graph.isEdgeConnected_two_iff_connected_and_forall_not_isBridge {α : Type u} {β : Type v} {G : Graph α β} (hV : G.vertexSet.Nonempty) : G.IsEdgeConnected 2 ↔ G.Connected ∧ ∀ (e : β), ¬G.IsBridge e

A multigraph with an actual vertex is 2-edge-connected exactly when it is connected and has no bridge.

theorem Graph.Walk.IsCycle.isEdgeConnected_two_walkGraph {α : Type u} {β : Type v} {G : Graph α β} {x : α} {p : G.Walk x x} (hp : p.IsCycle) : (G.walkGraph p).IsEdgeConnected 2

The graph traced by a cycle is 2-edge-connected.

Graphs from simple graphs

@[simp]

theorem Graph.isEdgeReachable_ofSimpleGraph_iff {α : Type u} (H : SimpleGraph α) (k : ℕ) (x y : α) : (ofSimpleGraph H).IsEdgeReachable k x y ↔ H.IsEdgeReachable (↑k) x y

Edge reachability in Graph.ofSimpleGraph H is simple-graph edge reachability in H.

@[simp]

theorem Graph.isEdgeConnected_ofSimpleGraph_iff {α : Type u} (H : SimpleGraph α) (k : ℕ) : (ofSimpleGraph H).IsEdgeConnected k ↔ H.IsEdgeConnected ↑k

Edge connectivity of Graph.ofSimpleGraph H is simple-graph edge connectivity of H.

theorem Graph.preconnected_and_forall_not_isBridge_ofSimpleGraph_iff {α : Type u} (H : SimpleGraph α) : (H.Preconnected ∧ ∀ (e : Sym2 α), ¬(ofSimpleGraph H).IsBridge e) ↔ ∀ (e : Sym2 α), ¬H.IsBridge e

On Graph.ofSimpleGraph H, the multigraph bridge criterion for 2-edge-connectivity agrees with Mathlib's simple-graph criterion SimpleGraph.isEdgeConnected_two_iff_forall_not_isBridge. The simple-graph criterion needs no separate reachability condition because SimpleGraph.IsBridge also holds for a non-edge joining distinct components, whereas multigraph bridges are actual edges.

Numerical invariants

noncomputable def Graph.edgeReachability {α : Type u} {β : Type v} (G : Graph α β) (x y : α) : ℕ∞

The local edge reachability of two points: the supremum in ℕ∞ of the natural thresholds k at which they are k-edge-reachable.

noncomputable def Graph.edgeConnectivity {α : Type u} {β : Type v} (G : Graph α β) : ℕ∞

The edge connectivity of a multigraph: the supremum in ℕ∞ of the natural thresholds k at which it is k-edge-connected. It is ⊤ when there is at most one actual vertex.

theorem Graph.isEdgeReachable_iff_le_edgeReachability {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (k : ℕ) : G.IsEdgeReachable k x y ↔ ↑k ≤ G.edgeReachability x y

Local edge reachability records exactly the thresholds at which edge reachability holds.

theorem Graph.isEdgeConnected_iff_le_edgeConnectivity {α : Type u} {β : Type v} {G : Graph α β} (k : ℕ) : G.IsEdgeConnected k ↔ ↑k ≤ G.edgeConnectivity

Edge connectivity records exactly the thresholds at which edge connectivity holds.

@[simp]

theorem Graph.edgeConnectivity_ofSimpleGraph {α : Type u} (H : SimpleGraph α) : (ofSimpleGraph H).edgeConnectivity = H.edgeConnectivity

The edge connectivity of Graph.ofSimpleGraph H is the edge connectivity of H.

theorem Graph.edgeReachability_comm {α : Type u} {β : Type v} {G : Graph α β} (x y : α) : G.edgeReachability x y = G.edgeReachability y x

theorem Graph.edgeReachability_self {α : Type u} {β : Type v} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : G.edgeReachability x x = ⊤

An actual vertex has local edge reachability ⊤ with itself.

theorem Graph.edgeConnectivity_eq_iInf_edgeReachability {α : Type u} {β : Type v} (G : Graph α β) : G.edgeConnectivity = ⨅ x ∈ G.vertexSet, ⨅ y ∈ G.vertexSet, G.edgeReachability x y

Edge connectivity is the infimum of the local edge reachabilities between actual vertices.

theorem Graph.edgeConnectivity_le_edgeReachability {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : G.edgeConnectivity ≤ G.edgeReachability x y

theorem Graph.edgeConnectivity_eq_top_of_subsingleton {α : Type u} {β : Type v} {G : Graph α β} (hG : G.vertexSet.Subsingleton) : G.edgeConnectivity = ⊤

A multigraph with at most one actual vertex has edge connectivity ⊤.

Bounds by incident edges

theorem Graph.IsEdgeReachable.le_nonloopIncidenceCount {α : Type u} {β : Type v} {G : Graph α β} {k : ℕ} {x y : α} (h : G.IsEdgeReachable k x y) (hxy : x ≠ y) (hfin : (incidenceSet x \ loopSet x).Finite) : k ≤ G.nonloopIncidenceCount x

If distinct points are k-edge-reachable, then the first one has at least k incident nonloop edges, provided it has finitely many nonloop incident edges.

theorem Graph.edgeReachability_le_nonloopIncidenceCount {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (hxy : x ≠ y) (hfin : (incidenceSet x \ loopSet x).Finite) : G.edgeReachability x y ≤ ↑(G.nonloopIncidenceCount x)

The local edge reachability between distinct points is at most the number of nonloop edges incident with the first, provided it has finitely many nonloop incident edges.

theorem Graph.edgeConnectivity_le_nonloopIncidenceCount {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) (hxy : x ≠ y) (hfin : (incidenceSet x \ loopSet x).Finite) : G.edgeConnectivity ≤ ↑(G.nonloopIncidenceCount x)

The edge connectivity of a multigraph with two distinct actual vertices is at most the number of nonloop edges at the first, provided it has finitely many nonloop incident edges.

theorem Graph.edgeConnectivity_eq_top_iff {α : Type u} {β : Type v} {G : Graph α β} [Finite ↑G.edgeSet] : G.edgeConnectivity = ⊤ ↔ G.vertexSet.Subsingleton

With finitely many actual edges, edge connectivity is ⊤ exactly when there is at most one actual vertex.

Two vertices joined by parallel edges

theorem Graph.reachable_banana_iff {α : Type u} {β : Type v} {u w : α} {F : Set β} (huw : u ≠ w) : (banana u w F).Reachable u w ↔ F.Nonempty

Two distinct vertices joined by the edges of F are reachable from each other exactly when F is nonempty.

theorem Graph.isEdgeReachable_banana_iff {α : Type u} {β : Type v} {k : ℕ} {u w : α} {F : Set β} (huw : u ≠ w) : (banana u w F).IsEdgeReachable k u w ↔ ↑k ≤ F.encard

Two distinct vertices joined by the parallel edges of F are k-edge-reachable exactly when there are at least k of these edges.

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

The local edge reachability of two distinct vertices joined by the parallel edges of F is the number of these edges.

theorem Graph.isEdgeConnected_banana_iff {α : Type u} {β : Type v} {k : ℕ} {u w : α} {F : Set β} (huw : u ≠ w) : (banana u w F).IsEdgeConnected k ↔ ↑k ≤ F.encard

Two distinct vertices joined by the parallel edges of F form a k-edge-connected graph exactly when there are at least k of these edges.

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

The edge connectivity of two distinct vertices joined by the parallel edges of F is the number of these edges; in particular a single edge gives edge connectivity 1.