Main definitions

• SimpleGraph.Reachable for the relation of whether there exists a walk between a given pair of vertices

• SimpleGraph.Preconnected and SimpleGraph.Connected are predicates on simple graphs for whether every vertex can be reached from every other, and in the latter case, whether the vertex type is nonempty.

• SimpleGraph.ConnectedComponent is the type of connected components of a given graph.

• SimpleGraph.IsBridge for whether an edge is a bridge edge

Main statements

• SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem characterizes bridge edges in terms of there being no cycle containing them.

Tags

trails, paths, cycles, bridge edges

Reachable and Connected

def SimpleGraph.Reachable {V : Type u} (G : SimpleGraph V) (u v : V) : Prop

Two vertices are reachable if there is a walk between them. This is equivalent to Relation.ReflTransGen of G.Adj. See SimpleGraph.reachable_iff_reflTransGen.

theorem SimpleGraph.reachable_iff_nonempty_univ {V : Type u} {G : SimpleGraph V} {u v : V} : G.Reachable u v ↔ Set.univ.Nonempty

theorem SimpleGraph.not_reachable_iff_isEmpty_walk {V : Type u} {G : SimpleGraph V} {u v : V} : ¬G.Reachable u v ↔ IsEmpty (G.Walk u v)

theorem SimpleGraph.Reachable.elim {V : Type u} {G : SimpleGraph V} {p : Prop} {u v : V} (h : G.Reachable u v) (hp : ∀ (a : G.Walk u v), p) : p

theorem SimpleGraph.Reachable.elim_path {V : Type u} {G : SimpleGraph V} {p : Prop} {u v : V} (h : G.Reachable u v) (hp : ∀ (a : G.Path u v), p) : p

theorem SimpleGraph.Walk.reachable {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : G.Reachable u v

theorem SimpleGraph.Adj.reachable {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : G.Reachable u v

theorem SimpleGraph.Reachable.refl {V : Type u} {G : SimpleGraph V} (u : V) : G.Reachable u u

theorem SimpleGraph.Reachable.rfl {V : Type u} {G : SimpleGraph V} {u : V} : G.Reachable u u

theorem SimpleGraph.Reachable.symm {V : Type u} {G : SimpleGraph V} {u v : V} (huv : G.Reachable u v) : G.Reachable v u

theorem SimpleGraph.reachable_comm {V : Type u} {G : SimpleGraph V} {u v : V} : G.Reachable u v ↔ G.Reachable v u

theorem SimpleGraph.Reachable.trans {V : Type u} {G : SimpleGraph V} {u v w : V} (huv : G.Reachable u v) (hvw : G.Reachable v w) : G.Reachable u w

theorem SimpleGraph.reachable_iff_reflTransGen {V : Type u} {G : SimpleGraph V} (u v : V) : G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v

theorem SimpleGraph.Reachable.map {V : Type u} {V' : Type v} {u v : V} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (h : G.Reachable u v) : G'.Reachable (f u) (f v)

theorem SimpleGraph.Reachable.mono {V : Type u} {u v : V} {G G' : SimpleGraph V} (h : G ≤ G') (Guv : G.Reachable u v) : G'.Reachable u v

theorem SimpleGraph.Reachable.exists_isPath {V : Type u} {G : SimpleGraph V} {u v : V} (hr : G.Reachable u v) : ∃ (p : G.Walk u v), p.IsPath

theorem SimpleGraph.Iso.reachable_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {u v : V} : G'.Reachable (φ u) (φ v) ↔ G.Reachable u v

theorem SimpleGraph.Iso.symm_apply_reachable {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {u : V} {v : V'} : G.Reachable (φ.symm v) u ↔ G'.Reachable v (φ u)

theorem SimpleGraph.Reachable.mem_subgraphVerts {V : Type u} {G : SimpleGraph V} {u v : V} {H : G.Subgraph} (hr : G.Reachable u v) (h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w) (hu : u ∈ H.verts) : v ∈ H.verts

@[irreducible]

theorem SimpleGraph.Reachable.mem_subgraphVerts.aux {V : Type u} {G : SimpleGraph V} {v : V} {H : G.Subgraph} (h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w) {v' : V} (hv' : v' ∈ H.verts) (p : G.Walk v' v) : v ∈ H.verts

theorem SimpleGraph.reachable_is_equivalence {V : Type u} (G : SimpleGraph V) : Equivalence G.Reachable

@[simp]

theorem SimpleGraph.reachable_bot {V : Type u} {u v : V} : ⊥.Reachable u v ↔ u = v

Distinct vertices are not reachable in the empty graph.

def SimpleGraph.reachableSetoid {V : Type u} (G : SimpleGraph V) : Setoid V

The equivalence relation on vertices given by SimpleGraph.Reachable.

def SimpleGraph.Preconnected {V : Type u} (G : SimpleGraph V) : Prop

A graph is preconnected if every pair of vertices is reachable from one another.

theorem SimpleGraph.Preconnected.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (f : G →g H) (hf : Function.Surjective ⇑f) (hG : G.Preconnected) : H.Preconnected

theorem SimpleGraph.Preconnected.mono {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') (hG : G.Preconnected) : G'.Preconnected

theorem SimpleGraph.bot_preconnected_iff_subsingleton {V : Type u} : ⊥.Preconnected ↔ Subsingleton V

theorem SimpleGraph.bot_preconnected {V : Type u} [Subsingleton V] : ⊥.Preconnected

theorem SimpleGraph.bot_not_preconnected {V : Type u} [Nontrivial V] : ¬⊥.Preconnected

theorem SimpleGraph.top_preconnected {V : Type u} : ⊤.Preconnected

theorem SimpleGraph.Iso.preconnected_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (e : G ≃g H) : G.Preconnected ↔ H.Preconnected

theorem SimpleGraph.Preconnected.support_eq_univ {V : Type u} [Nontrivial V] {G : SimpleGraph V} (h : G.Preconnected) : G.support = Set.univ

theorem SimpleGraph.adj_of_mem_walk_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : ¬p.Nil) {x : V} (hx : x ∈ p.support) : ∃ y ∈ p.support, G.Adj x y

theorem SimpleGraph.mem_support_of_mem_walk_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : ¬p.Nil) {w : V} (hw : w ∈ p.support) : w ∈ G.support

theorem SimpleGraph.mem_support_of_reachable {V : Type u} {G : SimpleGraph V} {u v : V} (huv : u ≠ v) (h : G.Reachable u v) : u ∈ G.support

theorem SimpleGraph.Preconnected.exists_isPath {V : Type u} {G : SimpleGraph V} (h : G.Preconnected) (u v : V) : ∃ (p : G.Walk u v), p.IsPath

structure SimpleGraph.Connected {V : Type u} (G : SimpleGraph V) : Prop

A graph is connected if it's preconnected and contains at least one vertex. This follows the convention observed by mathlib that something is connected iff it has exactly one connected component.

There is a CoeFun instance so that h u v can be used instead of h.Preconnected u v.

• preconnected : G.Preconnected
• nonempty : Nonempty V

theorem SimpleGraph.connected_iff {V : Type u} (G : SimpleGraph V) : G.Connected ↔ G.Preconnected ∧ Nonempty V

theorem SimpleGraph.connected_iff_exists_forall_reachable {V : Type u} (G : SimpleGraph V) : G.Connected ↔ ∃ (v : V), ∀ (w : V), G.Reachable v w

instance SimpleGraph.instCoeFunConnectedForallForallReachable {V : Type u} (G : SimpleGraph V) : CoeFun G.Connected fun (x : G.Connected) => ∀ (u v : V), G.Reachable u v

theorem SimpleGraph.Connected.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (f : G →g H) (hf : Function.Surjective ⇑f) (hG : G.Connected) : H.Connected

theorem SimpleGraph.Connected.mono {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') (hG : G.Connected) : G'.Connected

theorem SimpleGraph.Connected.exists_isPath {V : Type u} {G : SimpleGraph V} (h : G.Connected) (u v : V) : ∃ (p : G.Walk u v), p.IsPath

theorem SimpleGraph.bot_not_connected {V : Type u} [Nontrivial V] : ¬⊥.Connected

theorem SimpleGraph.top_connected {V : Type u} [Nonempty V] : ⊤.Connected

theorem SimpleGraph.Iso.connected_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (e : G ≃g H) : G.Connected ↔ H.Connected

def SimpleGraph.ConnectedComponent {V : Type u} (G : SimpleGraph V) : Type u

The quotient of V by the SimpleGraph.Reachable relation gives the connected components of a graph.

def SimpleGraph.connectedComponentMk {V : Type u} (G : SimpleGraph V) (v : V) : G.ConnectedComponent

Gives the connected component containing a particular vertex.

instance SimpleGraph.ConnectedComponent.inhabited {V : Type u} {G : SimpleGraph V} [Inhabited V] : Inhabited G.ConnectedComponent

@[simp]

theorem SimpleGraph.ConnectedComponent.inhabited_default {V : Type u} {G : SimpleGraph V} [Inhabited V] : default = G.connectedComponentMk default

instance SimpleGraph.ConnectedComponent.isEmpty {V : Type u} {G : SimpleGraph V} [IsEmpty V] : IsEmpty G.ConnectedComponent

theorem SimpleGraph.ConnectedComponent.ind {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponent → Prop} (h : ∀ (v : V), β (G.connectedComponentMk v)) (c : G.ConnectedComponent) : β c

theorem SimpleGraph.ConnectedComponent.ind₂ {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponent → G.ConnectedComponent → Prop} (h : ∀ (v w : V), β (G.connectedComponentMk v) (G.connectedComponentMk w)) (c d : G.ConnectedComponent) : β c d

theorem SimpleGraph.ConnectedComponent.sound {V : Type u} {G : SimpleGraph V} {v w : V} : G.Reachable v w → G.connectedComponentMk v = G.connectedComponentMk w

theorem SimpleGraph.ConnectedComponent.exact {V : Type u} {G : SimpleGraph V} {v w : V} : G.connectedComponentMk v = G.connectedComponentMk w → G.Reachable v w

@[simp]

theorem SimpleGraph.ConnectedComponent.eq {V : Type u} {G : SimpleGraph V} {v w : V} : G.connectedComponentMk v = G.connectedComponentMk w ↔ G.Reachable v w

theorem SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj {V : Type u} {G : SimpleGraph V} {v w : V} (a : G.Adj v w) : G.connectedComponentMk v = G.connectedComponentMk w

def SimpleGraph.ConnectedComponent.lift {V : Type u} {G : SimpleGraph V} {β : Sort u_1} (f : V → β) (h : ∀ (v w : V) (p : G.Walk v w), p.IsPath → f v = f w) : G.ConnectedComponent → β

The ConnectedComponent specialization of Quot.lift. Provides the stronger assumption that the vertices are connected by a path.

@[simp]

theorem SimpleGraph.ConnectedComponent.lift_mk {V : Type u} {G : SimpleGraph V} {β : Sort u_1} {f : V → β} {h : ∀ (v w : V) (p : G.Walk v w), p.IsPath → f v = f w} {v : V} : ConnectedComponent.lift f h (G.connectedComponentMk v) = f v

theorem SimpleGraph.ConnectedComponent.exists {V : Type u} {G : SimpleGraph V} {p : G.ConnectedComponent → Prop} : (∃ (c : G.ConnectedComponent), p c) ↔ ∃ (v : V), p (G.connectedComponentMk v)

theorem SimpleGraph.ConnectedComponent.forall {V : Type u} {G : SimpleGraph V} {p : G.ConnectedComponent → Prop} : (∀ (c : G.ConnectedComponent), p c) ↔ ∀ (v : V), p (G.connectedComponentMk v)

theorem SimpleGraph.Preconnected.subsingleton_connectedComponent {V : Type u} {G : SimpleGraph V} (h : G.Preconnected) : Subsingleton G.ConnectedComponent

def SimpleGraph.ConnectedComponent.recOn {V : Type u} {G : SimpleGraph V} {motive : G.ConnectedComponent → Sort u_1} (c : G.ConnectedComponent) (f : (v : V) → motive (G.connectedComponentMk v)) (h : ∀ (u v : V) (p : G.Walk u v), p.IsPath → ⋯ ▸ f u = f v) : motive c

This is Quot.recOn specialized to connected components. For convenience, it strengthens the assumptions in the hypothesis to provide a path between the vertices.

def SimpleGraph.ConnectedComponent.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G →g G') (C : G.ConnectedComponent) : G'.ConnectedComponent

The map on connected components induced by a graph homomorphism.

@[simp]

theorem SimpleGraph.ConnectedComponent.map_mk {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G →g G') (v : V) : map φ (G.connectedComponentMk v) = G'.connectedComponentMk (φ v)

@[simp]

theorem SimpleGraph.ConnectedComponent.map_id {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) : map Hom.id C = C

@[simp]

theorem SimpleGraph.ConnectedComponent.map_comp {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''} (C : G.ConnectedComponent) (φ : G →g G') (ψ : G' →g G'') : map ψ (map φ C) = map (ψ.comp φ) C

@[simp]

theorem SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {v : V} {C : G.ConnectedComponent} : G'.connectedComponentMk (φ v) = map (RelIso.toRelEmbedding φ).toRelHom C ↔ G.connectedComponentMk v = C

@[simp]

theorem SimpleGraph.ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {v' : V'} {C : G.ConnectedComponent} : G.connectedComponentMk (φ.symm v') = C ↔ G'.connectedComponentMk v' = map (RelIso.toRelEmbedding φ).toRelHom C

def SimpleGraph.Iso.connectedComponentEquiv {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') : G.ConnectedComponent ≃ G'.ConnectedComponent

An isomorphism of graphs induces a bijection of connected components.

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_symm_apply {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') (C : G'.ConnectedComponent) : φ.connectedComponentEquiv.symm C = ConnectedComponent.map (RelIso.toRelEmbedding φ.symm).toRelHom C

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_apply {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') (C : G.ConnectedComponent) : φ.connectedComponentEquiv C = ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_refl {V : Type u} {G : SimpleGraph V} : refl.connectedComponentEquiv = Equiv.refl G.ConnectedComponent

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_symm {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') : φ.symm.connectedComponentEquiv = φ.connectedComponentEquiv.symm

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_trans {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''} (φ : G ≃g G') (φ' : G' ≃g G'') : connectedComponentEquiv (RelIso.trans φ φ') = φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv

def SimpleGraph.ConnectedComponent.supp {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) : Set V

The set of vertices in a connected component of a graph.

theorem SimpleGraph.ConnectedComponent.supp_injective {V : Type u} {G : SimpleGraph V} : Function.Injective supp

theorem SimpleGraph.ConnectedComponent.supp_injective_iff {V : Type u} {G : SimpleGraph V} {a₁ a₂ : G.ConnectedComponent} : a₁ = a₂ ↔ a₁.supp = a₂.supp

@[simp]

theorem SimpleGraph.ConnectedComponent.supp_inj {V : Type u} {G : SimpleGraph V} {C D : G.ConnectedComponent} : C.supp = D.supp ↔ C = D

instance SimpleGraph.ConnectedComponent.instSetLike {V : Type u} {G : SimpleGraph V} : SetLike G.ConnectedComponent V

@[simp]

theorem SimpleGraph.ConnectedComponent.mem_supp_iff {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) (v : V) : v ∈ C.supp ↔ G.connectedComponentMk v = C

theorem SimpleGraph.ConnectedComponent.mem_supp_congr_adj {V : Type u} {G : SimpleGraph V} {v w : V} (c : G.ConnectedComponent) (hadj : G.Adj v w) : v ∈ c.supp ↔ w ∈ c.supp

theorem SimpleGraph.ConnectedComponent.connectedComponentMk_mem {V : Type u} {G : SimpleGraph V} {v : V} : v ∈ G.connectedComponentMk v

theorem SimpleGraph.ConnectedComponent.nonempty_supp {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) : C.supp.Nonempty

def SimpleGraph.ConnectedComponent.isoEquivSupp {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') (C : G.ConnectedComponent) : ↑C.supp ≃ ↑(φ.connectedComponentEquiv C).supp

The equivalence between connected components, induced by an isomorphism of graphs, itself defines an equivalence on the supports of each connected component.

theorem SimpleGraph.ConnectedComponent.mem_coe_supp_of_adj {V : Type u} {G : SimpleGraph V} {v w : V} {H : G.Subgraph} {c : H.coe.ConnectedComponent} (hv : v ∈ Subtype.val '' ↑c) (hw : w ∈ H.verts) (hadj : H.Adj v w) : w ∈ Subtype.val '' ↑c

theorem SimpleGraph.ConnectedComponent.eq_of_common_vertex {V : Type u} {G : SimpleGraph V} {v : V} {c c' : G.ConnectedComponent} (hc : v ∈ c.supp) (hc' : v ∈ c'.supp) : c = c'

theorem SimpleGraph.ConnectedComponent.connectedComponentMk_supp_subset_supp {V : Type u} {G G' : SimpleGraph V} {v : V} (h : G ≤ G') (c' : G'.ConnectedComponent) (hc' : v ∈ c'.supp) : (G.connectedComponentMk v).supp ⊆ c'.supp

theorem SimpleGraph.ConnectedComponent.biUnion_supp_eq_supp {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') (c' : G'.ConnectedComponent) : ⋃ (c : G.ConnectedComponent), ⋃ (_ : c.supp ⊆ c'.supp), c.supp = c'.supp

theorem SimpleGraph.ConnectedComponent.top_supp_eq_univ {V : Type u} (c : ⊤.ConnectedComponent) : c.supp = Set.univ

theorem SimpleGraph.ConnectedComponent.reachable_of_mem_supp {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C.supp) (hv : v ∈ C.supp) : G.Reachable u v

theorem SimpleGraph.ConnectedComponent.mem_supp_of_adj_mem_supp {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C.supp) (hadj : G.Adj u v) : v ∈ C.supp

def SimpleGraph.ConnectedComponent.toSimpleGraph {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) : SimpleGraph ↥C

Given a connected component C of a simple graph G, produce the induced graph on C. The declaration connected_toSimpleGraph shows it is connected, and toSimpleGraph_hom provides the homomorphism back to G.

def SimpleGraph.ConnectedComponent.toSimpleGraph_hom {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) : C.toSimpleGraph →g G

Homomorphism from a connected component graph to the original graph.

theorem SimpleGraph.ConnectedComponent.toSimpleGraph_hom_apply {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) (u : ↥C) : C.toSimpleGraph_hom u = ↑u

theorem SimpleGraph.ConnectedComponent.toSimpleGraph_adj {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C) (hv : v ∈ C) : C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨v, hv⟩ ↔ G.Adj u v

theorem SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph {V : Type u} {G : SimpleGraph V} {v w : V} (C : G.ConnectedComponent) : C.toSimpleGraph.spanningCoe.Adj v w ↔ v ∈ C.supp ∧ G.Adj v w

@[deprecated SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph (since := "2025-05-08")]

theorem SimpleGraph.ConnectedComponent.adj_spanningCoe_induce_supp {V : Type u} {G : SimpleGraph V} {v w : V} (C : G.ConnectedComponent) : C.toSimpleGraph.spanningCoe.Adj v w ↔ v ∈ C.supp ∧ G.Adj v w

Alias of SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph.

@[deprecated _private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected.0.SimpleGraph.ConnectedComponent.walk_toSimpleGraph' (since := "2025-05-08")]

def SimpleGraph.ConnectedComponent.reachable_induce_supp {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C) (hv : v ∈ C) (p : G.Walk u v) : C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩

Alias of _private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected.0.SimpleGraph.ConnectedComponent.walk_toSimpleGraph'.

---

Get the walk between two vertices in a connected component from a walk in the original graph.

noncomputable def SimpleGraph.ConnectedComponent.walk_toSimpleGraph {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C) (hv : v ∈ C) : C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩

There is a walk between every pair of vertices in a connected component.

theorem SimpleGraph.ConnectedComponent.reachable_toSimpleGraph {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C) (hv : v ∈ C) : C.toSimpleGraph.Reachable ⟨u, hu⟩ ⟨v, hv⟩

theorem SimpleGraph.ConnectedComponent.connected_toSimpleGraph {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) : C.toSimpleGraph.Connected

@[deprecated SimpleGraph.ConnectedComponent.connected_toSimpleGraph (since := "2025-05-08")]

theorem SimpleGraph.ConnectedComponent.connected_induce_supp {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) : C.toSimpleGraph.Connected

Alias of SimpleGraph.ConnectedComponent.connected_toSimpleGraph.

theorem SimpleGraph.pairwise_disjoint_supp_connectedComponent {V : Type u} (G : SimpleGraph V) : Pairwise fun (c c' : G.ConnectedComponent) => Disjoint c.supp c'.supp

theorem SimpleGraph.iUnion_connectedComponentSupp {V : Type u} (G : SimpleGraph V) : ⋃ (c : G.ConnectedComponent), c.supp = Set.univ

theorem SimpleGraph.Preconnected.set_univ_walk_nonempty {V : Type u} {G : SimpleGraph V} (hconn : G.Preconnected) (u v : V) : Set.univ.Nonempty

theorem SimpleGraph.Connected.set_univ_walk_nonempty {V : Type u} {G : SimpleGraph V} (hconn : G.Connected) (u v : V) : Set.univ.Nonempty

Bridge edges

def SimpleGraph.IsBridge {V : Type u} (G : SimpleGraph V) (e : Sym2 V) : Prop

An edge of a graph is a bridge if, after removing it, its incident vertices are no longer reachable from one another.

theorem SimpleGraph.isBridge_iff {V : Type u} {G : SimpleGraph V} {u v : V} : G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬(G \ fromEdgeSet {s(u, v)}).Reachable u v

theorem SimpleGraph.reachable_delete_edges_iff_exists_walk {V : Type u} {G : SimpleGraph V} {v w v' w' : V} : (G \ fromEdgeSet {s(v, w)}).Reachable v' w' ↔ ∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges

theorem SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges {V : Type u} {G : SimpleGraph V} {v w : V} : G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges

theorem SimpleGraph.reachable_deleteEdges_iff_exists_cycle.aux {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges) (c : G.Walk u u) (hc : c.IsTrail) (he : s(v, w) ∈ c.edges) (hw : w ∈ (c.takeUntil v ⋯).support) : False

theorem SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle {V : Type u} {G : SimpleGraph V} {v w : V} : G.Adj v w ∧ (G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges

theorem SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem {V : Type u} {G : SimpleGraph V} {v w : V} : G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

@[deprecated SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem (since := "2025-05-23")]

theorem SimpleGraph.isBridge_iff_adj_and_forall_cycle_not_mem {V : Type u} {G : SimpleGraph V} {v w : V} : G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Alias of SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem.

theorem SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem {V : Type u} {G : SimpleGraph V} {e : Sym2 V} : G.IsBridge e ↔ e ∈ G.edgeSet ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges

@[deprecated SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem (since := "2025-05-23")]

theorem SimpleGraph.isBridge_iff_mem_and_forall_cycle_not_mem {V : Type u} {G : SimpleGraph V} {e : Sym2 V} : G.IsBridge e ↔ e ∈ G.edgeSet ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges

Alias of SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem.

theorem SimpleGraph.Connected.connected_delete_edge_of_not_isBridge {V : Type u} {G : SimpleGraph V} (hG : G.Connected) {x y : V} (h : ¬G.IsBridge s(x, y)) : (G.deleteEdges {s(x, y)}).Connected

Deleting a non-bridge edge from a connected graph preserves connectedness.