Edge Connectivity

This file defines k-edge-connectivity for simple graphs.

Main definitions

• SimpleGraph.IsEdgeReachable: Two vertices are k-edge-reachable if they remain reachable after removing strictly fewer than k edges.
• SimpleGraph.IsEdgeConnected: A graph is k-edge-connected if any two vertices are k-edge-reachable.

def SimpleGraph.IsEdgeReachable {V : Type u_1} (G : SimpleGraph V) (k : ℕ) (u v : V) : Prop

Two vertices are k-edge-reachable if they remain reachable after removing strictly fewer than k edges.

def SimpleGraph.IsEdgeConnected {V : Type u_1} (G : SimpleGraph V) (k : ℕ) : Prop

A graph is k-edge-connected if any two vertices are k-edge-reachable.

@[simp]

theorem SimpleGraph.IsEdgeReachable.refl {V : Type u_1} {G : SimpleGraph V} {k : ℕ} (u : V) : G.IsEdgeReachable k u u

@[deprecated SimpleGraph.IsEdgeReachable.refl (since := "2026-01-06")]

theorem SimpleGraph.IsEdgeReachable.rfl {V : Type u_1} {G : SimpleGraph V} {k : ℕ} (u : V) : G.IsEdgeReachable k u u

Alias of SimpleGraph.IsEdgeReachable.refl.

theorem SimpleGraph.IsEdgeReachable.symm {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v : V} (h : G.IsEdgeReachable k u v) : G.IsEdgeReachable k v u

theorem SimpleGraph.isEdgeReachable_comm {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v : V} : G.IsEdgeReachable k u v ↔ G.IsEdgeReachable k v u

theorem SimpleGraph.IsEdgeReachable.trans {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v w : V} (h1 : G.IsEdgeReachable k u v) (h2 : G.IsEdgeReachable k v w) : G.IsEdgeReachable k u w

theorem SimpleGraph.IsEdgeReachable.mono {V : Type u_1} {G H : SimpleGraph V} {k : ℕ} {u v : V} (hGH : G ≤ H) (h : G.IsEdgeReachable k u v) : H.IsEdgeReachable k u v

theorem SimpleGraph.IsEdgeReachable.anti {V : Type u_1} {G : SimpleGraph V} {k l : ℕ} {u v : V} (hkl : k ≤ l) (h : G.IsEdgeReachable l u v) : G.IsEdgeReachable k u v

@[simp]

theorem SimpleGraph.IsEdgeReachable.zero {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.IsEdgeReachable 0 u v

@[simp]

theorem SimpleGraph.IsEdgeConnected.zero {V : Type u_1} {G : SimpleGraph V} : G.IsEdgeConnected 0

@[simp]

theorem SimpleGraph.isEdgeReachable_one {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.IsEdgeReachable 1 u v ↔ G.Reachable u v

@[simp]

theorem SimpleGraph.isEdgeConnected_one {V : Type u_1} {G : SimpleGraph V} : G.IsEdgeConnected 1 ↔ G.Preconnected

theorem SimpleGraph.IsEdgeReachable.reachable {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v : V} (hk : k ≠ 0) (huv : G.IsEdgeReachable k u v) : G.Reachable u v

theorem SimpleGraph.IsEdgeConnected.preconnected {V : Type u_1} {G : SimpleGraph V} {k : ℕ} (hk : k ≠ 0) (h : G.IsEdgeConnected k) : G.Preconnected

theorem SimpleGraph.IsEdgeConnected.connected {V : Type u_1} {G : SimpleGraph V} {k : ℕ} [Nonempty V] (hk : k ≠ 0) (h : G.IsEdgeConnected k) : G.Connected

theorem SimpleGraph.isEdgeReachable_add_one {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v : V} (hk : k ≠ 0) : G.IsEdgeReachable (k + 1) u v ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v

theorem SimpleGraph.isEdgeConnected_add_one {V : Type u_1} {G : SimpleGraph V} {k : ℕ} (hk : k ≠ 0) : G.IsEdgeConnected (k + 1) ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeConnected k

theorem SimpleGraph.isBridge_iff_adj_and_not_isEdgeConnected_two {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬G.IsEdgeReachable 2 u v

An edge is a bridge iff its endpoints are adjacent and not 2-edge-reachable.

theorem SimpleGraph.isEdgeReachable_two {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.IsEdgeReachable 2 u v ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).Reachable u v

theorem SimpleGraph.isEdgeConnected_two {V : Type u_1} {G : SimpleGraph V} : G.IsEdgeConnected 2 ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).Preconnected

A graph is 2-edge-connected iff it has no bridge.

2-reachability

In this section, we prove results about 2-connected components of a graph, but without naming them.

theorem SimpleGraph.Walk.IsTrail.not_mem_edges_of_not_isEdgeReachable_two {V : Type u_1} {G : SimpleGraph V} {u v x : V} {w : G.Walk u v} (hw : w.IsTrail) (huv : G.IsEdgeReachable 2 u v) (huy : ¬G.IsEdgeReachable 2 u x) : x ∉ w.support

A trail doesn't go through a vertex that is not 2-edge-reachable from its 2-edge-reachable endpoints.