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.

theorem SimpleGraph.isEdgeConnected_iff {V : Type u_1} {G : SimpleGraph V} {k : ℕ∞} : G.IsEdgeConnected k ↔ ∀ ⦃s : Set (Sym2 V)⦄, s.encard < k → (G.deleteEdges s).Preconnected

@[simp]

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

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

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.IsEdgeReachable.of_subsingleton {V : Type u_1} {G : SimpleGraph V} {k : ℕ∞} {u v : V} [Subsingleton V] : G.IsEdgeReachable k u v

theorem SimpleGraph.IsEdgeConnected.of_subsingleton {V : Type u_1} {G : SimpleGraph V} {k : ℕ∞} [Subsingleton V] : G.IsEdgeConnected k

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.le_degree {V : Type u_1} {G : SimpleGraph V} {k : ℕ∞} {u v : V} [Fintype ↑(G.neighborSet u)] (h : G.IsEdgeReachable k u v) (huv : u ≠ v) : k ≤ ↑(G.degree u)

theorem SimpleGraph.IsEdgeConnected.le_degree {V : Type u_1} {G : SimpleGraph V} {k : ℕ∞} {u : V} [Fintype ↑(G.neighborSet u)] [Nontrivial V] (h : G.IsEdgeConnected k) : k ≤ ↑(G.degree u)

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.not_isEdgeReachable_two {V : Type u_1} {G : SimpleGraph V} {u v : V} (huv : G.IsBridge s(u, v)) : ¬G.IsEdgeReachable 2 u v

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

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

The forward direction of this is true without assuming u and v are adjacent. See IsBridge.not_isEdgeReachable_two.

@[deprecated SimpleGraph.isBridge_iff_not_isEdgeReachable_two (since := "2026-05-16")]

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

Alias of SimpleGraph.isBridge_iff_not_isEdgeReachable_two.

---

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

The forward direction of this is true without assuming u and v are adjacent. See IsBridge.not_isEdgeReachable_two.

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_iff_forall_preconnected {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 remains preconnected after removing any edge.

@[deprecated SimpleGraph.isEdgeConnected_two_iff_forall_preconnected (since := "2026-10-01")]

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

Alias of SimpleGraph.isEdgeConnected_two_iff_forall_preconnected.

---

A graph is 2-edge-connected iff it remains preconnected after removing any edge.

theorem SimpleGraph.isEdgeConnected_two_iff_forall_not_isBridge {V : Type u_1} {G : SimpleGraph V} : G.IsEdgeConnected 2 ↔ ∀ (e : Sym2 V), ¬G.IsBridge e

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

theorem SimpleGraph.exists_adj_isEdgeReachable_two {V : Type u_1} {G : SimpleGraph V} {u v : V} (hne : u ≠ v) (h : G.IsEdgeReachable 2 u v) : ∃ (w : V), G.Adj u w ∧ G.IsEdgeReachable 2 u w

theorem SimpleGraph.isEdgeReachable_top_iff_forall_finite {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.IsEdgeReachable ⊤ u v ↔ ∀ ⦃s : Set (Sym2 V)⦄, s.Finite → (G.deleteEdges s).Reachable u v

theorem SimpleGraph.isEdgeConnected_top_iff_forall_finite {V : Type u_1} {G : SimpleGraph V} : G.IsEdgeConnected ⊤ ↔ ∀ ⦃s : Set (Sym2 V)⦄, s.Finite → (G.deleteEdges s).Preconnected

theorem SimpleGraph.isEdgeReachable_top_iff_forall_nat {V : Type u_1} {G : SimpleGraph V} {u v : V} : G.IsEdgeReachable ⊤ u v ↔ ∀ (n : ℕ), G.IsEdgeReachable (↑n) u v

theorem SimpleGraph.isEdgeConnected_top_iff_forall_nat {V : Type u_1} {G : SimpleGraph V} : G.IsEdgeConnected ⊤ ↔ ∀ (n : ℕ), G.IsEdgeConnected ↑n

2-reachability

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

theorem SimpleGraph.Walk.IsTrail.isEdgeReachable_two_of_isEdgeReachable_two {V : Type u_1} {G : SimpleGraph V} {u v x y : V} {w : G.Walk u v} (hw : w.IsTrail) (huv : G.IsEdgeReachable 2 u v) (hx : x ∈ w.support) (hy : y ∈ w.support) : G.IsEdgeReachable 2 x y

Vertices of a trail with 2-edge reachable endpoints are 2-edge reachable.

theorem SimpleGraph.Walk.IsTrail.isEdgeReachable_two {V : Type u_1} {G : SimpleGraph V} {u x y : V} {w : G.Walk u u} (hw : w.IsTrail) (hx : x ∈ w.support) (hy : y ∈ w.support) : G.IsEdgeReachable 2 x y

Vertices of a closed trail are 2-edge reachable.