Documentation

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Main definitions #

Main statements #

Tags #

trails, paths, cycles, bridge edges

Reachable and Connected #

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

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.

Equations
Instances For
    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.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 : vH.verts, ∀ (w : V), G.Adj v wH.Adj v w) (hu : u H.verts) :
    @[irreducible]
    theorem SimpleGraph.Reachable.mem_subgraphVerts.aux {V : Type u} {G : SimpleGraph V} {v : V} {H : G.Subgraph} (h : vH.verts, ∀ (w : V), G.Adj v wH.Adj v w) {v' : V} (hv' : v' H.verts) (p : G.Walk v' v) :
    @[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.

    The equivalence relation on vertices given by SimpleGraph.Reachable.

    Equations
    Instances For

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

      Equations
      Instances For
        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) :
        theorem SimpleGraph.Preconnected.mono {V : Type u} {G G' : SimpleGraph V} (h : G G') (hG : G.Preconnected) :
        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) :
        yp.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) :
        theorem SimpleGraph.mem_support_of_reachable {V : Type u} {G : SimpleGraph V} {u v : V} (huv : u v) (h : G.Reachable u v) :
        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) :

        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.

        Instances For
          theorem SimpleGraph.connected_iff_exists_forall_reachable {V : Type u} (G : SimpleGraph V) :
          G.Connected ∃ (v : V), ∀ (w : V), G.Reachable v w
          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) :
          theorem SimpleGraph.Connected.mono {V : Type u} {G G' : SimpleGraph V} (h : G G') (hG : 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.Iso.connected_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (e : G ≃g H) :

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

          Equations
          Instances For

            Gives the connected component containing a particular vertex.

            Equations
            Instances For
              theorem SimpleGraph.ConnectedComponent.ind {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponentProp} (h : ∀ (v : V), β (G.connectedComponentMk v)) (c : G.ConnectedComponent) :
              β c
              theorem SimpleGraph.ConnectedComponent.ind₂ {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponentG.ConnectedComponentProp} (h : ∀ (v w : V), β (G.connectedComponentMk v) (G.connectedComponentMk w)) (c d : G.ConnectedComponent) :
              β c d
              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.IsPathf v = f w) :

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

              Equations
              Instances For
                @[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.IsPathf v = f w} {v : V} :
                theorem SimpleGraph.ConnectedComponent.exists {V : Type u} {G : SimpleGraph V} {p : G.ConnectedComponentProp} :
                (∃ (c : G.ConnectedComponent), p c) ∃ (v : V), p (G.connectedComponentMk v)
                theorem SimpleGraph.ConnectedComponent.forall {V : Type u} {G : SimpleGraph V} {p : G.ConnectedComponentProp} :
                (∀ (c : G.ConnectedComponent), p c) ∀ (v : V), p (G.connectedComponentMk v)
                def SimpleGraph.ConnectedComponent.recOn {V : Type u} {G : SimpleGraph V} {motive : G.ConnectedComponentSort 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.

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

                  The map on connected components induced by a graph homomorphism.

                  Equations
                  Instances For
                    @[simp]
                    theorem SimpleGraph.ConnectedComponent.map_mk {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G →g G') (v : V) :
                    @[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

                    An isomorphism of graphs induces a bijection of connected components.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]

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

                      Equations
                      Instances For
                        theorem SimpleGraph.ConnectedComponent.supp_injective_iff {V : Type u} {G : SimpleGraph V} {a₁ a₂ : G.ConnectedComponent} :
                        a₁ = a₂ a₁.supp = a₂.supp
                        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

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          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) :
                          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.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.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

                          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.

                          Equations
                          Instances For

                            Homomorphism from a connected component graph to the original graph.

                            Equations
                            Instances For
                              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
                              @[deprecated SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph (since := "2025-05-08")]

                              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) :

                              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.

                              Equations
                              Instances For
                                noncomputable def SimpleGraph.ConnectedComponent.walk_toSimpleGraph {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u C) (hv : v C) :

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

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

                                  Alias of SimpleGraph.ConnectedComponent.connected_toSimpleGraph.

                                  Bridge edges #

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

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

                                  Equations
                                  Instances For
                                    theorem SimpleGraph.isBridge_iff {V : Type u} {G : SimpleGraph V} {u v : 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) :
                                    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.IsCycles(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.IsCycles(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.IsCycleep.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.IsCycleep.edges

                                    Alias of SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem.

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