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.

TODO

IsBridge is unpractical: we shouldn't require the edge to be present. See https://github.com/leanprover-community/mathlib4/issues/31690.

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.adj_le_reachable {V : Type u} (G : SimpleGraph V) : G.Adj ≤ G.Reachable

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

@[simp]

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_eq_reflTransGen {V : Type u} {G : SimpleGraph V} : G.Reachable = Relation.ReflTransGen G.Adj

theorem SimpleGraph.reachable_fromEdgeSet_eq_reflTransGen_toRel {V : Type u} {s : Set (Sym2 V)} : (fromEdgeSet s).Reachable = Relation.ReflTransGen (Sym2.ToRel s)

theorem SimpleGraph.reachable_fromEdgeSet_fromRel_eq_reflTransGen {V : Type u} {r : V → V → Prop} (sym : Symmetric r) : (fromEdgeSet (Sym2.fromRel sym)).Reachable = Relation.ReflTransGen r

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.mono' {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') : G.Reachable ≤ G'.Reachable

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

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.

@[simp]

theorem SimpleGraph.reachable_top {V : Type u} {u v : V} : (completeGraph V).Reachable u v

theorem SimpleGraph.Reachable.of_subsingleton {V : Type u} {G : SimpleGraph V} [Subsingleton V] {u v : V} : G.Reachable u v

theorem SimpleGraph.not_reachable_of_left_degree_zero {V : Type u} {G : SimpleGraph V} {u v : V} [Fintype ↑(G.neighborSet u)] (huv : u ≠ v) (hu : G.degree u = 0) : ¬G.Reachable u v

theorem SimpleGraph.not_reachable_of_right_degree_zero {V : Type u} {G : SimpleGraph V} {u v : V} [Fintype ↑(G.neighborSet v)] (huv : u ≠ v) (hu : G.degree v = 0) : ¬G.Reachable u v

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.preconnected_iff_reachable_eq_top {V : Type u} (G : SimpleGraph V) : G.Preconnected ↔ G.Reachable = ⊤

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

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

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

@[simp]

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

@[deprecated SimpleGraph.preconnected_bot (since := "2025-09-23")]

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

Alias of SimpleGraph.preconnected_bot.

@[deprecated SimpleGraph.preconnected_bot_iff_subsingleton (since := "2025-09-23")]

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

Alias of SimpleGraph.preconnected_bot_iff_subsingleton.

@[deprecated SimpleGraph.not_preconnected_bot (since := "2025-09-23")]

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

Alias of SimpleGraph.not_preconnected_bot.

@[deprecated SimpleGraph.preconnected_top (since := "2025-09-23")]

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

Alias of SimpleGraph.preconnected_top.

theorem SimpleGraph.Preconnected.of_subsingleton {V : Type u} {G : SimpleGraph V} [Subsingleton V] : G.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.Preconnected.degree_pos_of_nontrivial {V : Type u} [Nontrivial V] {G : SimpleGraph V} (h : G.Preconnected) (v : V) [Fintype ↑(G.neighborSet v)] : 0 < G.degree v

theorem SimpleGraph.Preconnected.minDegree_pos_of_nontrivial {V : Type u} [Nontrivial V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (h : G.Preconnected) : 0 < G.minDegree

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.connected_bot_iff {V : Type u} : ⊥.Connected ↔ Subsingleton V ∧ Nonempty V

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

theorem SimpleGraph.connected_top_iff {V : Type u} : (completeGraph V).Connected ↔ Nonempty V

@[simp]

theorem SimpleGraph.connected_top {V : Type u} [Nonempty V] : (completeGraph V).Connected

@[deprecated SimpleGraph.not_connected_bot (since := "2025-09-23")]

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

Alias of SimpleGraph.not_connected_bot.

@[deprecated SimpleGraph.connected_top (since := "2025-09-23")]

theorem SimpleGraph.top_connected {V : Type u} [Nonempty V] : (completeGraph V).Connected

Alias of SimpleGraph.connected_top.

theorem SimpleGraph.Connected.of_subsingleton {V : Type u} {G : SimpleGraph V} [Nonempty V] [Subsingleton V] : G.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

theorem SimpleGraph.reachable_or_compl_adj {V : Type u} (G : SimpleGraph V) (u v : V) : G.Reachable u v ∨ Gᶜ.Adj u v

theorem SimpleGraph.reachable_or_reachable_compl {V : Type u} (G : SimpleGraph V) (u v w : V) : G.Reachable u v ∨ Gᶜ.Reachable u w

theorem SimpleGraph.connected_or_preconnected_compl {V : Type u} (G : SimpleGraph V) : G.Connected ∨ Gᶜ.Preconnected

theorem SimpleGraph.connected_or_connected_compl {V : Type u} (G : SimpleGraph V) [Nonempty V] : G.Connected ∨ Gᶜ.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

instance SimpleGraph.ConnectedComponent.instSubsingleton {V : Type u} {G : SimpleGraph V} [Subsingleton V] : Subsingleton G.ConnectedComponent

instance SimpleGraph.ConnectedComponent.instUnique {V : Type u} {G : SimpleGraph V} [Unique V] : Unique G.ConnectedComponent

instance SimpleGraph.ConnectedComponent.instNonempty {V : Type u} {G : SimpleGraph V} [Nonempty V] : Nonempty G.ConnectedComponent

instance SimpleGraph.ConnectedComponent.instFinite {V : Type u} {G : SimpleGraph V} [Finite V] : Finite 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.surjective_map_ofLE {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') : Function.Surjective (map (Hom.ofLE h))

@[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_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_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_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

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⟩

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

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

theorem SimpleGraph.ConnectedComponent.maximal_connected_induce_supp {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) : Maximal (fun (x : Set V) => (induce x G).Connected) C.supp

theorem SimpleGraph.ConnectedComponent.maximal_connected_induce_iff {V : Type u} {G : SimpleGraph V} (s : Set V) : Maximal (fun (x : Set V) => (induce x G).Connected) s ↔ ∃ (C : G.ConnectedComponent), C.supp = s

def SimpleGraph.homOfConnectedComponents {V : Type u} {V' : Type v} (G : SimpleGraph V) {H : SimpleGraph V'} (C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H) : G →g H

Given graph homomorphisms from each connected component of G to H, this is the graph homomorphism from G to H.

@[simp]

theorem SimpleGraph.homOfConnectedComponents_apply {V : Type u} {V' : Type v} (G : SimpleGraph V) {H : SimpleGraph V'} (C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H) (x : V) : (G.homOfConnectedComponents C) x = (C (G.connectedComponentMk x)) ⟨x, ⋯⟩

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

theorem SimpleGraph.Preconnected.exists_adj_of_nontrivial {V : Type u} [Nontrivial V] {G : SimpleGraph V} (h : G.Preconnected) (v : V) : ∃ (u : V), G.Adj v u

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

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

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.

theorem SimpleGraph.IsBridge.anti_of_mem_edgeSet {V : Type u} {G G' : SimpleGraph V} {e : Sym2 V} (hle : G ≤ G') (h : e ∈ G.edgeSet) (h' : G'.IsBridge e) : G.IsBridge e

If e is an edge in G and is a bridge in a larger graph G', then it's a bridge in G.

2-reachability

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

theorem SimpleGraph.Walk.exists_mem_edges_of_not_reachable_deleteEdges {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {s : Set (Sym2 V)} (huv : ¬(G.deleteEdges s).Reachable u v) : ∃ e ∈ s, e ∈ w.edges

A walk between two vertices separated by a set of edges must go through one of those edges.

theorem SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {e : Sym2 V} (huv : ¬(G.deleteEdges {e}).Reachable u v) : e ∈ w.edges

A walk between two vertices separated by an edge must go through that edge.

theorem SimpleGraph.Walk.IsTrail.not_mem_edges_of_not_reachable {V : Type u} {G : SimpleGraph V} {u v x y : V} {w : G.Walk u v} (hw : w.IsTrail) (huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y) (hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y) : s(x, y) ∉ w.edges

A trail doesn't go through an edge that disconnects one of its endpoints from the endpoints of the trail.

theorem SimpleGraph.Walk.IsTrail.not_mem_support_of_not_reachable {V : Type u} {G : SimpleGraph V} {u v x y : V} {w : G.Walk u v} (hw : w.IsTrail) (huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y) (hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y) : y ∉ w.support

A trail doesn't go through a vertex that is disconnected from its endpoints by an edge.

theorem SimpleGraph.Walk.IsTrail.not_mem_support_of_subsingleton_neighborSet {V : Type u} {G : SimpleGraph V} {u v x : V} {w : G.Walk u v} (hw : w.IsTrail) (hxu : x ≠ u) (hxv : x ≠ v) (hx : (G.neighborSet x).Subsingleton) : x ∉ w.support

A trail doesn't go through any leaf vertex, except possibly at its endpoints.

theorem SimpleGraph.Preconnected.induce_of_degree_eq_one {V : Type u} {G : SimpleGraph V} (hG : G.Preconnected) {s : Set V} (hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton) : (induce s G).Preconnected

Removing leaves from a connected graph keeps it connected.