Documentation

Mathlib.Combinatorics.SimpleGraph.Connectivity

Graph connectivity #

In a simple graph,

Warning: graph theorists mean something different by "path" than do homotopy theorists. A "walk" in graph theory is a "path" in homotopy theory. Another warning: some graph theorists use "path" and "simple path" for "walk" and "path."

Some definitions and theorems have inspiration from multigraph counterparts in [Chou1994].

Main definitions #

Main statements #

Tags #

walks, trails, paths, circuits, cycles, bridge edges

inductive SimpleGraph.Walk {V : Type u} (G : SimpleGraph V) :
VVType u

A walk is a sequence of adjacent vertices. For vertices u v : V, the type walk u v consists of all walks starting at u and ending at v.

We say that a walk visits the vertices it contains. The set of vertices a walk visits is SimpleGraph.Walk.support.

See SimpleGraph.Walk.nil' and SimpleGraph.Walk.cons' for patterns that can be useful in definitions since they make the vertices explicit.

  • nil: {V : Type u} → {G : SimpleGraph V} → {u : V} → G.Walk u u
  • cons: {V : Type u} → {G : SimpleGraph V} → {u v w : V} → G.Adj u vG.Walk v wG.Walk u w
Instances For
    instance SimpleGraph.instDecidableEqWalk :
    {V : Type u_1} → {G : SimpleGraph V} → {a a_1 : V} → [inst : DecidableEq V] → DecidableEq (G.Walk a a_1)
    Equations
    • SimpleGraph.instDecidableEqWalk = SimpleGraph.decEqWalk✝
    @[simp]
    theorem SimpleGraph.Walk.instInhabited_default {V : Type u} (G : SimpleGraph V) (v : V) :
    default = SimpleGraph.Walk.nil
    instance SimpleGraph.Walk.instInhabited {V : Type u} (G : SimpleGraph V) (v : V) :
    Inhabited (G.Walk v v)
    Equations
    @[reducible, match_pattern]
    def SimpleGraph.Adj.toWalk {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) :
    G.Walk u v

    The one-edge walk associated to a pair of adjacent vertices.

    Equations
    Instances For
      @[reducible, match_pattern, inline]
      abbrev SimpleGraph.Walk.nil' {V : Type u} {G : SimpleGraph V} (u : V) :
      G.Walk u u

      Pattern to get Walk.nil with the vertex as an explicit argument.

      Equations
      Instances For
        @[reducible, match_pattern, inline]
        abbrev SimpleGraph.Walk.cons' {V : Type u} {G : SimpleGraph V} (u : V) (v : V) (w : V) (h : G.Adj u v) (p : G.Walk v w) :
        G.Walk u w

        Pattern to get Walk.cons with the vertices as explicit arguments.

        Equations
        Instances For
          def SimpleGraph.Walk.copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
          G.Walk u' v'

          Change the endpoints of a walk using equalities. This is helpful for relaxing definitional equality constraints and to be able to state otherwise difficult-to-state lemmas. While this is a simple wrapper around Eq.rec, it gives a canonical way to write it.

          The simp-normal form is for the copy to be pushed outward. That way calculations can occur within the "copy context."

          Equations
          • p.copy hu hv = huhvp
          Instances For
            @[simp]
            theorem SimpleGraph.Walk.copy_rfl_rfl {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
            p.copy = p
            @[simp]
            theorem SimpleGraph.Walk.copy_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} {u'' : V} {v'' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
            (p.copy hu hv).copy hu' hv' = p.copy
            @[simp]
            theorem SimpleGraph.Walk.copy_nil {V : Type u} {G : SimpleGraph V} {u : V} {u' : V} (hu : u = u') :
            SimpleGraph.Walk.nil.copy hu hu = SimpleGraph.Walk.nil
            theorem SimpleGraph.Walk.copy_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {u' : V} {w' : V} (h : G.Adj u v) (p : G.Walk v w) (hu : u = u') (hw : w = w') :
            (SimpleGraph.Walk.cons h p).copy hu hw = SimpleGraph.Walk.cons (p.copy hw)
            @[simp]
            theorem SimpleGraph.Walk.cons_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {v' : V} {w' : V} (h : G.Adj u v) (p : G.Walk v' w') (hv : v' = v) (hw : w' = w) :
            SimpleGraph.Walk.cons h (p.copy hv hw) = (SimpleGraph.Walk.cons p).copy hw
            theorem SimpleGraph.Walk.exists_eq_cons_of_ne {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (hne : u v) (p : G.Walk u v) :
            ∃ (w : V) (h : G.Adj u w) (p' : G.Walk w v), p = SimpleGraph.Walk.cons h p'
            def SimpleGraph.Walk.length {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
            G.Walk u v

            The length of a walk is the number of edges/darts along it.

            Equations
            Instances For
              def SimpleGraph.Walk.append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} :
              G.Walk u vG.Walk v wG.Walk u w

              The concatenation of two compatible walks.

              Equations
              Instances For
                def SimpleGraph.Walk.concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
                G.Walk u w

                The reversed version of SimpleGraph.Walk.cons, concatenating an edge to the end of a walk.

                Equations
                Instances For
                  theorem SimpleGraph.Walk.concat_eq_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
                  p.concat h = p.append (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)
                  def SimpleGraph.Walk.reverseAux {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} :
                  G.Walk u vG.Walk u wG.Walk v w

                  The concatenation of the reverse of the first walk with the second walk.

                  Equations
                  Instances For
                    def SimpleGraph.Walk.reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (w : G.Walk u v) :
                    G.Walk v u

                    The walk in reverse.

                    Equations
                    • w.reverse = w.reverseAux SimpleGraph.Walk.nil
                    Instances For
                      def SimpleGraph.Walk.getVert {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                      G.Walk u vV

                      Get the nth vertex from a walk, where n is generally expected to be between 0 and p.length, inclusive. If n is greater than or equal to p.length, the result is the path's endpoint.

                      Equations
                      Instances For
                        @[simp]
                        theorem SimpleGraph.Walk.getVert_zero {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (w : G.Walk u v) :
                        w.getVert 0 = u
                        theorem SimpleGraph.Walk.getVert_of_length_le {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (w : G.Walk u v) {i : } (hi : w.length i) :
                        w.getVert i = v
                        @[simp]
                        theorem SimpleGraph.Walk.getVert_length {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (w : G.Walk u v) :
                        w.getVert w.length = v
                        theorem SimpleGraph.Walk.adj_getVert_succ {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (w : G.Walk u v) {i : } (hi : i < w.length) :
                        G.Adj (w.getVert i) (w.getVert (i + 1))
                        @[simp]
                        theorem SimpleGraph.Walk.cons_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (h : G.Adj u v) (p : G.Walk v w) (q : G.Walk w x) :
                        (SimpleGraph.Walk.cons h p).append q = SimpleGraph.Walk.cons h (p.append q)
                        @[simp]
                        theorem SimpleGraph.Walk.cons_nil_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
                        (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).append p = SimpleGraph.Walk.cons h p
                        @[simp]
                        theorem SimpleGraph.Walk.append_nil {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                        p.append SimpleGraph.Walk.nil = p
                        @[simp]
                        theorem SimpleGraph.Walk.nil_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                        SimpleGraph.Walk.nil.append p = p
                        theorem SimpleGraph.Walk.append_assoc {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk v w) (r : G.Walk w x) :
                        p.append (q.append r) = (p.append q).append r
                        @[simp]
                        theorem SimpleGraph.Walk.append_copy_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {u' : V} {v' : V} {w' : V} (p : G.Walk u v) (q : G.Walk v w) (hu : u = u') (hv : v = v') (hw : w = w') :
                        (p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw
                        theorem SimpleGraph.Walk.concat_nil {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) :
                        SimpleGraph.Walk.nil.concat h = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
                        @[simp]
                        theorem SimpleGraph.Walk.concat_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (h : G.Adj u v) (p : G.Walk v w) (h' : G.Adj w x) :
                        (SimpleGraph.Walk.cons h p).concat h' = SimpleGraph.Walk.cons h (p.concat h')
                        theorem SimpleGraph.Walk.append_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk v w) (h : G.Adj w x) :
                        p.append (q.concat h) = (p.append q).concat h
                        theorem SimpleGraph.Walk.concat_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (h : G.Adj v w) (q : G.Walk w x) :
                        (p.concat h).append q = p.append (SimpleGraph.Walk.cons h q)
                        theorem SimpleGraph.Walk.exists_cons_eq_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
                        ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w), SimpleGraph.Walk.cons h p = q.concat h'

                        A non-trivial cons walk is representable as a concat walk.

                        theorem SimpleGraph.Walk.exists_concat_eq_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
                        ∃ (x : V) (h' : G.Adj u x) (q : G.Walk x w), p.concat h = SimpleGraph.Walk.cons h' q

                        A non-trivial concat walk is representable as a cons walk.

                        @[simp]
                        theorem SimpleGraph.Walk.reverse_nil {V : Type u} {G : SimpleGraph V} {u : V} :
                        SimpleGraph.Walk.nil.reverse = SimpleGraph.Walk.nil
                        theorem SimpleGraph.Walk.reverse_singleton {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) :
                        (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).reverse = SimpleGraph.Walk.cons SimpleGraph.Walk.nil
                        @[simp]
                        theorem SimpleGraph.Walk.cons_reverseAux {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk w x) (h : G.Adj w u) :
                        (SimpleGraph.Walk.cons h p).reverseAux q = p.reverseAux (SimpleGraph.Walk.cons q)
                        @[simp]
                        theorem SimpleGraph.Walk.append_reverseAux {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk v w) (r : G.Walk u x) :
                        (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)
                        @[simp]
                        theorem SimpleGraph.Walk.reverseAux_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk u w) (r : G.Walk w x) :
                        (p.reverseAux q).append r = p.reverseAux (q.append r)
                        theorem SimpleGraph.Walk.reverseAux_eq_reverse_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk u w) :
                        p.reverseAux q = p.reverse.append q
                        @[simp]
                        theorem SimpleGraph.Walk.reverse_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
                        (SimpleGraph.Walk.cons h p).reverse = p.reverse.append (SimpleGraph.Walk.cons SimpleGraph.Walk.nil)
                        @[simp]
                        theorem SimpleGraph.Walk.reverse_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
                        (p.copy hu hv).reverse = p.reverse.copy hv hu
                        @[simp]
                        theorem SimpleGraph.Walk.reverse_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
                        (p.append q).reverse = q.reverse.append p.reverse
                        @[simp]
                        theorem SimpleGraph.Walk.reverse_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
                        (p.concat h).reverse = SimpleGraph.Walk.cons p.reverse
                        @[simp]
                        theorem SimpleGraph.Walk.reverse_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                        p.reverse.reverse = p
                        @[simp]
                        theorem SimpleGraph.Walk.length_nil {V : Type u} {G : SimpleGraph V} {u : V} :
                        SimpleGraph.Walk.nil.length = 0
                        @[simp]
                        theorem SimpleGraph.Walk.length_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
                        (SimpleGraph.Walk.cons h p).length = p.length + 1
                        @[simp]
                        theorem SimpleGraph.Walk.length_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
                        (p.copy hu hv).length = p.length
                        @[simp]
                        theorem SimpleGraph.Walk.length_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
                        (p.append q).length = p.length + q.length
                        @[simp]
                        theorem SimpleGraph.Walk.length_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
                        (p.concat h).length = p.length + 1
                        @[simp]
                        theorem SimpleGraph.Walk.length_reverseAux {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk u w) :
                        (p.reverseAux q).length = p.length + q.length
                        @[simp]
                        theorem SimpleGraph.Walk.length_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                        p.reverse.length = p.length
                        theorem SimpleGraph.Walk.eq_of_length_eq_zero {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} :
                        p.length = 0u = v
                        theorem SimpleGraph.Walk.adj_of_length_eq_one {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} :
                        p.length = 1G.Adj u v
                        @[simp]
                        theorem SimpleGraph.Walk.exists_length_eq_zero_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                        (∃ (p : G.Walk u v), p.length = 0) u = v
                        @[simp]
                        theorem SimpleGraph.Walk.length_eq_zero_iff {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} :
                        p.length = 0 p = SimpleGraph.Walk.nil
                        theorem SimpleGraph.Walk.getVert_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) (i : ) :
                        (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
                        theorem SimpleGraph.Walk.getVert_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (i : ) :
                        p.reverse.getVert i = p.getVert (p.length - i)
                        def SimpleGraph.Walk.concatRecAux {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u vSort u_1} (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil) (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v pmotive u w (p.concat h)) {u : V} {v : V} (p : G.Walk u v) :
                        motive v u p.reverse

                        Auxiliary definition for SimpleGraph.Walk.concatRec

                        Equations
                        Instances For
                          def SimpleGraph.Walk.concatRec {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u vSort u_1} (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil) (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v pmotive u w (p.concat h)) {u : V} {v : V} (p : G.Walk u v) :
                          motive u v p

                          Recursor on walks by inducting on SimpleGraph.Walk.concat.

                          This is inducting from the opposite end of the walk compared to SimpleGraph.Walk.rec, which inducts on SimpleGraph.Walk.cons.

                          Equations
                          Instances For
                            @[simp]
                            theorem SimpleGraph.Walk.concatRec_nil {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u vSort u_1} (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil) (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v pmotive u w (p.concat h)) (u : V) :
                            SimpleGraph.Walk.concatRec Hnil Hconcat SimpleGraph.Walk.nil = Hnil
                            @[simp]
                            theorem SimpleGraph.Walk.concatRec_concat {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u vSort u_1} (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil) (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v pmotive u w (p.concat h)) {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
                            SimpleGraph.Walk.concatRec Hnil Hconcat (p.concat h) = Hconcat p h (SimpleGraph.Walk.concatRec Hnil Hconcat p)
                            theorem SimpleGraph.Walk.concat_ne_nil {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (h : G.Adj v u) :
                            p.concat h SimpleGraph.Walk.nil
                            theorem SimpleGraph.Walk.concat_inj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {v' : V} {w : V} {p : G.Walk u v} {h : G.Adj v w} {p' : G.Walk u v'} {h' : G.Adj v' w} (he : p.concat h = p'.concat h') :
                            ∃ (hv : v = v'), p.copy hv = p'
                            def SimpleGraph.Walk.support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                            G.Walk u vList V

                            The support of a walk is the list of vertices it visits in order.

                            Equations
                            Instances For
                              def SimpleGraph.Walk.darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                              G.Walk u vList G.Dart

                              The darts of a walk is the list of darts it visits in order.

                              Equations
                              Instances For
                                def SimpleGraph.Walk.edges {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :

                                The edges of a walk is the list of edges it visits in order. This is defined to be the list of edges underlying SimpleGraph.Walk.darts.

                                Equations
                                • p.edges = List.map SimpleGraph.Dart.edge p.darts
                                Instances For
                                  @[simp]
                                  theorem SimpleGraph.Walk.support_nil {V : Type u} {G : SimpleGraph V} {u : V} :
                                  SimpleGraph.Walk.nil.support = [u]
                                  @[simp]
                                  theorem SimpleGraph.Walk.support_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
                                  (SimpleGraph.Walk.cons h p).support = u :: p.support
                                  @[simp]
                                  theorem SimpleGraph.Walk.support_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
                                  (p.concat h).support = p.support.concat w
                                  @[simp]
                                  theorem SimpleGraph.Walk.support_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
                                  (p.copy hu hv).support = p.support
                                  theorem SimpleGraph.Walk.support_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
                                  (p.append p').support = p.support ++ p'.support.tail
                                  @[simp]
                                  theorem SimpleGraph.Walk.support_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  p.reverse.support = p.support.reverse
                                  @[simp]
                                  theorem SimpleGraph.Walk.support_ne_nil {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  p.support []
                                  theorem SimpleGraph.Walk.tail_support_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
                                  (p.append p').support.tail = p.support.tail ++ p'.support.tail
                                  theorem SimpleGraph.Walk.support_eq_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  p.support = u :: p.support.tail
                                  @[simp]
                                  theorem SimpleGraph.Walk.start_mem_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  u p.support
                                  @[simp]
                                  theorem SimpleGraph.Walk.end_mem_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  v p.support
                                  @[simp]
                                  theorem SimpleGraph.Walk.support_nonempty {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  {w : V | w p.support}.Nonempty
                                  theorem SimpleGraph.Walk.mem_support_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) :
                                  w p.support w = u w p.support.tail
                                  theorem SimpleGraph.Walk.mem_support_nil_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                                  u SimpleGraph.Walk.nil.support u = v
                                  @[simp]
                                  theorem SimpleGraph.Walk.mem_tail_support_append_iff {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
                                  t (p.append p').support.tail t p.support.tail t p'.support.tail
                                  @[simp]
                                  theorem SimpleGraph.Walk.end_mem_tail_support_of_ne {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : u v) (p : G.Walk u v) :
                                  v p.support.tail
                                  @[simp]
                                  theorem SimpleGraph.Walk.mem_support_append_iff {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
                                  t (p.append p').support t p.support t p'.support
                                  @[simp]
                                  theorem SimpleGraph.Walk.subset_support_append_left {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
                                  p.support (p.append q).support
                                  @[simp]
                                  theorem SimpleGraph.Walk.subset_support_append_right {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
                                  q.support (p.append q).support
                                  theorem SimpleGraph.Walk.coe_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  p.support = {u} + p.support.tail
                                  theorem SimpleGraph.Walk.coe_support_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
                                  (p.append p').support = {u} + p.support.tail + p'.support.tail
                                  theorem SimpleGraph.Walk.coe_support_append' {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
                                  (p.append p').support = p.support + p'.support - {v}
                                  theorem SimpleGraph.Walk.chain_adj_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
                                  List.Chain G.Adj u p.support
                                  theorem SimpleGraph.Walk.chain'_adj_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  List.Chain' G.Adj p.support
                                  theorem SimpleGraph.Walk.chain_dartAdj_darts {V : Type u} {G : SimpleGraph V} {d : G.Dart} {v : V} {w : V} (h : d.toProd.2 = v) (p : G.Walk v w) :
                                  List.Chain G.DartAdj d p.darts
                                  theorem SimpleGraph.Walk.chain'_dartAdj_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  List.Chain' G.DartAdj p.darts
                                  theorem SimpleGraph.Walk.edges_subset_edgeSet {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) ⦃e : Sym2 V :
                                  e p.edgese G.edgeSet

                                  Every edge in a walk's edge list is an edge of the graph. It is written in this form (rather than using ) to avoid unsightly coercions.

                                  theorem SimpleGraph.Walk.adj_of_mem_edges {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {x : V} {y : V} (p : G.Walk u v) (h : s(x, y) p.edges) :
                                  G.Adj x y
                                  @[simp]
                                  theorem SimpleGraph.Walk.darts_nil {V : Type u} {G : SimpleGraph V} {u : V} :
                                  SimpleGraph.Walk.nil.darts = []
                                  @[simp]
                                  theorem SimpleGraph.Walk.darts_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
                                  (SimpleGraph.Walk.cons h p).darts = { toProd := (u, v), adj := h } :: p.darts
                                  @[simp]
                                  theorem SimpleGraph.Walk.darts_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
                                  (p.concat h).darts = p.darts.concat { toProd := (v, w), adj := h }
                                  @[simp]
                                  theorem SimpleGraph.Walk.darts_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
                                  (p.copy hu hv).darts = p.darts
                                  @[simp]
                                  theorem SimpleGraph.Walk.darts_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
                                  (p.append p').darts = p.darts ++ p'.darts
                                  @[simp]
                                  theorem SimpleGraph.Walk.darts_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  p.reverse.darts = (List.map SimpleGraph.Dart.symm p.darts).reverse
                                  theorem SimpleGraph.Walk.mem_darts_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {d : G.Dart} {p : G.Walk u v} :
                                  d p.reverse.darts d.symm p.darts
                                  theorem SimpleGraph.Walk.cons_map_snd_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  u :: List.map (fun (x : G.Dart) => x.toProd.2) p.darts = p.support
                                  theorem SimpleGraph.Walk.map_snd_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  List.map (fun (x : G.Dart) => x.toProd.2) p.darts = p.support.tail
                                  theorem SimpleGraph.Walk.map_fst_darts_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  List.map (fun (x : G.Dart) => x.toProd.1) p.darts ++ [v] = p.support
                                  theorem SimpleGraph.Walk.map_fst_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  List.map (fun (x : G.Dart) => x.toProd.1) p.darts = p.support.dropLast
                                  @[simp]
                                  theorem SimpleGraph.Walk.edges_nil {V : Type u} {G : SimpleGraph V} {u : V} :
                                  SimpleGraph.Walk.nil.edges = []
                                  @[simp]
                                  theorem SimpleGraph.Walk.edges_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
                                  (SimpleGraph.Walk.cons h p).edges = s(u, v) :: p.edges
                                  @[simp]
                                  theorem SimpleGraph.Walk.edges_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
                                  (p.concat h).edges = p.edges.concat s(v, w)
                                  @[simp]
                                  theorem SimpleGraph.Walk.edges_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
                                  (p.copy hu hv).edges = p.edges
                                  @[simp]
                                  theorem SimpleGraph.Walk.edges_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
                                  (p.append p').edges = p.edges ++ p'.edges
                                  @[simp]
                                  theorem SimpleGraph.Walk.edges_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  p.reverse.edges = p.edges.reverse
                                  @[simp]
                                  theorem SimpleGraph.Walk.length_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  p.support.length = p.length + 1
                                  @[simp]
                                  theorem SimpleGraph.Walk.length_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  p.darts.length = p.length
                                  @[simp]
                                  theorem SimpleGraph.Walk.length_edges {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                  p.edges.length = p.length
                                  theorem SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {d : G.Dart} :
                                  d p.dartsd.toProd.1 p.support
                                  theorem SimpleGraph.Walk.dart_snd_mem_support_of_mem_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {d : G.Dart} (h : d p.darts) :
                                  d.toProd.2 p.support
                                  theorem SimpleGraph.Walk.fst_mem_support_of_mem_edges {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} {w : V} (p : G.Walk v w) (he : s(t, u) p.edges) :
                                  t p.support
                                  theorem SimpleGraph.Walk.snd_mem_support_of_mem_edges {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} {w : V} (p : G.Walk v w) (he : s(t, u) p.edges) :
                                  u p.support
                                  theorem SimpleGraph.Walk.darts_nodup_of_support_nodup {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (h : p.support.Nodup) :
                                  p.darts.Nodup
                                  theorem SimpleGraph.Walk.edges_nodup_of_support_nodup {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (h : p.support.Nodup) :
                                  p.edges.Nodup
                                  inductive SimpleGraph.Walk.Nil {V : Type u} {G : SimpleGraph V} {v : V} {w : V} :
                                  G.Walk v wProp

                                  Predicate for the empty walk.

                                  Solves the dependent type problem where p = G.Walk.nil typechecks only if p has defeq endpoints.

                                  • nil: ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.Nil
                                  Instances For
                                    @[simp]
                                    theorem SimpleGraph.Walk.nil_nil {V : Type u} {G : SimpleGraph V} {u : V} :
                                    SimpleGraph.Walk.nil.Nil
                                    @[simp]
                                    theorem SimpleGraph.Walk.not_nil_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {h : G.Adj u v} {p : G.Walk v w} :
                                    instance SimpleGraph.Walk.instDecidableNil {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : G.Walk v w) :
                                    Decidable p.Nil
                                    Equations
                                    theorem SimpleGraph.Walk.Nil.eq {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} :
                                    p.Nilv = w
                                    theorem SimpleGraph.Walk.not_nil_of_ne {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} :
                                    v w¬p.Nil
                                    theorem SimpleGraph.Walk.nil_iff_support_eq {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} :
                                    p.Nil p.support = [v]
                                    theorem SimpleGraph.Walk.nil_iff_length_eq {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} :
                                    p.Nil p.length = 0
                                    theorem SimpleGraph.Walk.not_nil_iff {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} :
                                    ¬p.Nil ∃ (u : V) (h : G.Adj v u) (q : G.Walk u w), p = SimpleGraph.Walk.cons h q
                                    theorem SimpleGraph.Walk.nil_iff_eq_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} :
                                    p.Nil p = SimpleGraph.Walk.nil

                                    A walk with its endpoints defeq is Nil if and only if it is equal to nil.

                                    theorem SimpleGraph.Walk.Nil.eq_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} :
                                    p.Nilp = SimpleGraph.Walk.nil

                                    Alias of the forward direction of SimpleGraph.Walk.nil_iff_eq_nil.


                                    A walk with its endpoints defeq is Nil if and only if it is equal to nil.

                                    def SimpleGraph.Walk.notNilRec {V : Type u} {G : SimpleGraph V} {u : V} {w : V} {motive : {u w : V} → (p : G.Walk u w) → ¬p.NilSort u_1} (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (SimpleGraph.Walk.cons h q) ) (p : G.Walk u w) (hp : ¬p.Nil) :
                                    motive p hp
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def SimpleGraph.Walk.sndOfNotNil {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) :
                                      V

                                      The second vertex along a non-nil walk.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem SimpleGraph.Walk.adj_sndOfNotNil {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} (hp : ¬p.Nil) :
                                        G.Adj v (p.sndOfNotNil hp)
                                        def SimpleGraph.Walk.tail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (hp : ¬p.Nil) :
                                        G.Walk (p.sndOfNotNil hp) v

                                        The walk obtained by removing the first dart of a non-nil walk.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem SimpleGraph.Walk.firstDart_toProd {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) :
                                          (p.firstDart hp).toProd = (v, p.sndOfNotNil hp)
                                          def SimpleGraph.Walk.firstDart {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) :
                                          G.Dart

                                          The first dart of a walk.

                                          Equations
                                          • p.firstDart hp = { toProd := (v, p.sndOfNotNil hp), adj := }
                                          Instances For
                                            theorem SimpleGraph.Walk.edge_firstDart {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) :
                                            (p.firstDart hp).edge = s(v, p.sndOfNotNil hp)
                                            @[simp]
                                            theorem SimpleGraph.Walk.cons_tail_eq {V : Type u} {G : SimpleGraph V} {x : V} {y : V} (p : G.Walk x y) (hp : ¬p.Nil) :
                                            SimpleGraph.Walk.cons (p.tail hp) = p
                                            @[simp]
                                            theorem SimpleGraph.Walk.cons_support_tail {V : Type u} {G : SimpleGraph V} {x : V} {y : V} (p : G.Walk x y) (hp : ¬p.Nil) :
                                            x :: (p.tail hp).support = p.support
                                            @[simp]
                                            theorem SimpleGraph.Walk.length_tail_add_one {V : Type u} {G : SimpleGraph V} {x : V} {y : V} {p : G.Walk x y} (hp : ¬p.Nil) :
                                            (p.tail hp).length + 1 = p.length
                                            @[simp]
                                            theorem SimpleGraph.Walk.nil_copy {V : Type u} {G : SimpleGraph V} {x : V} {y : V} {x' : V} {y' : V} {p : G.Walk x y} (hx : x = x') (hy : y = y') :
                                            (p.copy hx hy).Nil = p.Nil
                                            @[simp]
                                            theorem SimpleGraph.Walk.support_tail {V : Type u} {G : SimpleGraph V} {v : V} (p : G.Walk v v) (hp : ¬p.Nil) :
                                            (p.tail hp).support = p.support.tail

                                            Trails, paths, circuits, cycles #

                                            theorem SimpleGraph.Walk.isTrail_def {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                            p.IsTrail p.edges.Nodup
                                            structure SimpleGraph.Walk.IsTrail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :

                                            A trail is a walk with no repeating edges.

                                            • edges_nodup : p.edges.Nodup
                                            Instances For
                                              theorem SimpleGraph.Walk.IsTrail.edges_nodup {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (self : p.IsTrail) :
                                              p.edges.Nodup
                                              structure SimpleGraph.Walk.IsPath {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) extends SimpleGraph.Walk.IsTrail :

                                              A path is a walk with no repeating vertices. Use SimpleGraph.Walk.IsPath.mk' for a simpler constructor.

                                              • edges_nodup : p.edges.Nodup
                                              • support_nodup : p.support.Nodup
                                              Instances For
                                                theorem SimpleGraph.Walk.IsPath.support_nodup {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (self : p.IsPath) :
                                                p.support.Nodup
                                                theorem SimpleGraph.Walk.IsPath.isTrail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (h : p.IsPath) :
                                                p.IsTrail
                                                theorem SimpleGraph.Walk.isCircuit_def {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) :
                                                p.IsCircuit p.IsTrail p SimpleGraph.Walk.nil
                                                structure SimpleGraph.Walk.IsCircuit {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) extends SimpleGraph.Walk.IsTrail :

                                                A circuit at u : V is a nonempty trail beginning and ending at u.

                                                • edges_nodup : p.edges.Nodup
                                                • ne_nil : p SimpleGraph.Walk.nil
                                                Instances For
                                                  theorem SimpleGraph.Walk.IsCircuit.ne_nil {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (self : p.IsCircuit) :
                                                  p SimpleGraph.Walk.nil
                                                  theorem SimpleGraph.Walk.IsCircuit.isTrail {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (h : p.IsCircuit) :
                                                  p.IsTrail
                                                  structure SimpleGraph.Walk.IsCycle {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) extends SimpleGraph.Walk.IsCircuit :

                                                  A cycle at u : V is a circuit at u whose only repeating vertex is u (which appears exactly twice).

                                                  • edges_nodup : p.edges.Nodup
                                                  • ne_nil : p SimpleGraph.Walk.nil
                                                  • support_nodup : p.support.tail.Nodup
                                                  Instances For
                                                    theorem SimpleGraph.Walk.IsCycle.support_nodup {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (self : p.IsCycle) :
                                                    p.support.tail.Nodup
                                                    theorem SimpleGraph.Walk.IsCycle.isCircuit {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (h : p.IsCycle) :
                                                    p.IsCircuit
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.isTrail_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
                                                    (p.copy hu hv).IsTrail p.IsTrail
                                                    theorem SimpleGraph.Walk.IsPath.mk' {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (h : p.support.Nodup) :
                                                    p.IsPath
                                                    theorem SimpleGraph.Walk.isPath_def {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                    p.IsPath p.support.Nodup
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.isPath_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
                                                    (p.copy hu hv).IsPath p.IsPath
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.isCircuit_copy {V : Type u} {G : SimpleGraph V} {u : V} {u' : V} (p : G.Walk u u) (hu : u = u') :
                                                    (p.copy hu hu).IsCircuit p.IsCircuit
                                                    theorem SimpleGraph.Walk.IsCircuit.not_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCircuit) :
                                                    ¬p.Nil
                                                    theorem SimpleGraph.Walk.isCycle_def {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) :
                                                    p.IsCycle p.IsTrail p SimpleGraph.Walk.nil p.support.tail.Nodup
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.isCycle_copy {V : Type u} {G : SimpleGraph V} {u : V} {u' : V} (p : G.Walk u u) (hu : u = u') :
                                                    (p.copy hu hu).IsCycle p.IsCycle
                                                    theorem SimpleGraph.Walk.IsCycle.not_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) :
                                                    ¬p.Nil
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.IsTrail.nil {V : Type u} {G : SimpleGraph V} {u : V} :
                                                    SimpleGraph.Walk.nil.IsTrail
                                                    theorem SimpleGraph.Walk.IsTrail.of_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {h : G.Adj u v} {p : G.Walk v w} :
                                                    (SimpleGraph.Walk.cons h p).IsTrailp.IsTrail
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.cons_isTrail_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
                                                    (SimpleGraph.Walk.cons h p).IsTrail p.IsTrail s(u, v)p.edges
                                                    theorem SimpleGraph.Walk.IsTrail.reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (h : p.IsTrail) :
                                                    p.reverse.IsTrail
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.reverse_isTrail_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                    p.reverse.IsTrail p.IsTrail
                                                    theorem SimpleGraph.Walk.IsTrail.of_append_left {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) :
                                                    p.IsTrail
                                                    theorem SimpleGraph.Walk.IsTrail.of_append_right {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) :
                                                    q.IsTrail
                                                    theorem SimpleGraph.Walk.IsTrail.count_edges_le_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : G.Walk u v} (h : p.IsTrail) (e : Sym2 V) :
                                                    List.count e p.edges 1
                                                    theorem SimpleGraph.Walk.IsTrail.count_edges_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : G.Walk u v} (h : p.IsTrail) {e : Sym2 V} (he : e p.edges) :
                                                    List.count e p.edges = 1
                                                    theorem SimpleGraph.Walk.IsPath.nil {V : Type u} {G : SimpleGraph V} {u : V} :
                                                    SimpleGraph.Walk.nil.IsPath
                                                    theorem SimpleGraph.Walk.IsPath.of_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {h : G.Adj u v} {p : G.Walk v w} :
                                                    (SimpleGraph.Walk.cons h p).IsPathp.IsPath
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.cons_isPath_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
                                                    (SimpleGraph.Walk.cons h p).IsPath p.IsPath up.support
                                                    theorem SimpleGraph.Walk.IsPath.cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk v w} (hp : p.IsPath) (hu : up.support) {h : G.Adj u v} :
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.isPath_iff_eq_nil {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) :
                                                    p.IsPath p = SimpleGraph.Walk.nil
                                                    theorem SimpleGraph.Walk.IsPath.reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (h : p.IsPath) :
                                                    p.reverse.IsPath
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.isPath_reverse_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                    p.reverse.IsPath p.IsPath
                                                    theorem SimpleGraph.Walk.IsPath.of_append_left {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} :
                                                    (p.append q).IsPathp.IsPath
                                                    theorem SimpleGraph.Walk.IsPath.of_append_right {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsPath) :
                                                    q.IsPath
                                                    @[simp]
                                                    theorem SimpleGraph.Walk.IsCycle.not_of_nil {V : Type u} {G : SimpleGraph V} {u : V} :
                                                    ¬SimpleGraph.Walk.nil.IsCycle
                                                    theorem SimpleGraph.Walk.IsCycle.ne_bot {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} :
                                                    p.IsCycleG
                                                    theorem SimpleGraph.Walk.IsCycle.three_le_length {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) :
                                                    3 p.length
                                                    theorem SimpleGraph.Walk.cons_isCycle_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk v u) (h : G.Adj u v) :
                                                    (SimpleGraph.Walk.cons h p).IsCycle p.IsPath s(u, v)p.edges
                                                    theorem SimpleGraph.Walk.IsPath.tail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (hp : p.IsPath) (hp' : ¬p.Nil) :
                                                    (p.tail hp').IsPath

                                                    About paths #

                                                    instance SimpleGraph.Walk.instDecidableIsPathOfDecidableEq {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) :
                                                    Decidable p.IsPath
                                                    Equations
                                                    • p.instDecidableIsPathOfDecidableEq = .mpr inferInstance
                                                    theorem SimpleGraph.Walk.IsPath.length_lt {V : Type u} {G : SimpleGraph V} [Fintype V] {u : V} {v : V} {p : G.Walk u v} (hp : p.IsPath) :
                                                    p.length < Fintype.card V

                                                    Walk decompositions #

                                                    def SimpleGraph.Walk.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : V} (p : G.Walk v w) (u : V) :
                                                    u p.supportG.Walk v u

                                                    Given a vertex in the support of a path, give the path up until (and including) that vertex.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    • SimpleGraph.Walk.nil.takeUntil x x_1 = .mpr SimpleGraph.Walk.nil
                                                    Instances For
                                                      def SimpleGraph.Walk.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : V} (p : G.Walk v w) (u : V) :
                                                      u p.supportG.Walk u w

                                                      Given a vertex in the support of a path, give the path from (and including) that vertex to the end. In other words, drop vertices from the front of a path until (and not including) that vertex.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      • SimpleGraph.Walk.nil.dropUntil x x_1 = .mpr SimpleGraph.Walk.nil
                                                      Instances For
                                                        @[simp]
                                                        theorem SimpleGraph.Walk.take_spec {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
                                                        (p.takeUntil u h).append (p.dropUntil u h) = p

                                                        The takeUntil and dropUntil functions split a walk into two pieces. The lemma SimpleGraph.Walk.count_support_takeUntil_eq_one specifies where this split occurs.

                                                        theorem SimpleGraph.Walk.mem_support_iff_exists_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk u v} :
                                                        w p.support ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r
                                                        @[simp]
                                                        theorem SimpleGraph.Walk.count_support_takeUntil_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
                                                        List.count u (p.takeUntil u h).support = 1
                                                        theorem SimpleGraph.Walk.count_edges_takeUntil_le_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) (x : V) :
                                                        List.count s(u, x) (p.takeUntil u h).edges 1
                                                        @[simp]
                                                        theorem SimpleGraph.Walk.takeUntil_copy {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {v' : V} {w' : V} (p : G.Walk v w) (hv : v = v') (hw : w = w') (h : u (p.copy hv hw).support) :
                                                        (p.copy hv hw).takeUntil u h = (p.takeUntil u ).copy hv
                                                        @[simp]
                                                        theorem SimpleGraph.Walk.dropUntil_copy {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {v' : V} {w' : V} (p : G.Walk v w) (hv : v = v') (hw : w = w') (h : u (p.copy hv hw).support) :
                                                        (p.copy hv hw).dropUntil u h = (p.dropUntil u ).copy hw
                                                        theorem SimpleGraph.Walk.support_takeUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
                                                        (p.takeUntil u h).support p.support
                                                        theorem SimpleGraph.Walk.support_dropUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
                                                        (p.dropUntil u h).support p.support
                                                        theorem SimpleGraph.Walk.darts_takeUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
                                                        (p.takeUntil u h).darts p.darts
                                                        theorem SimpleGraph.Walk.darts_dropUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
                                                        (p.dropUntil u h).darts p.darts
                                                        theorem SimpleGraph.Walk.edges_takeUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
                                                        (p.takeUntil u h).edges p.edges
                                                        theorem SimpleGraph.Walk.edges_dropUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
                                                        (p.dropUntil u h).edges p.edges
                                                        theorem SimpleGraph.Walk.length_takeUntil_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
                                                        (p.takeUntil u h).length p.length
                                                        theorem SimpleGraph.Walk.length_dropUntil_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
                                                        (p.dropUntil u h).length p.length
                                                        theorem SimpleGraph.Walk.IsTrail.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u p.support) :
                                                        (p.takeUntil u h).IsTrail
                                                        theorem SimpleGraph.Walk.IsTrail.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u p.support) :
                                                        (p.dropUntil u h).IsTrail
                                                        theorem SimpleGraph.Walk.IsPath.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u p.support) :
                                                        (p.takeUntil u h).IsPath
                                                        theorem SimpleGraph.Walk.IsPath.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u p.support) :
                                                        (p.dropUntil u h).IsPath
                                                        def SimpleGraph.Walk.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (c : G.Walk v v) (h : u c.support) :
                                                        G.Walk u u

                                                        Rotate a loop walk such that it is centered at the given vertex.

                                                        Equations
                                                        • c.rotate h = (c.dropUntil u h).append (c.takeUntil u h)
                                                        Instances For
                                                          @[simp]
                                                          theorem SimpleGraph.Walk.support_rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (c : G.Walk v v) (h : u c.support) :
                                                          (c.rotate h).support.tail ~r c.support.tail
                                                          theorem SimpleGraph.Walk.rotate_darts {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (c : G.Walk v v) (h : u c.support) :
                                                          (c.rotate h).darts ~r c.darts
                                                          theorem SimpleGraph.Walk.rotate_edges {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (c : G.Walk v v) (h : u c.support) :
                                                          (c.rotate h).edges ~r c.edges
                                                          theorem SimpleGraph.Walk.IsTrail.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {c : G.Walk v v} (hc : c.IsTrail) (h : u c.support) :
                                                          (c.rotate h).IsTrail
                                                          theorem SimpleGraph.Walk.IsCircuit.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {c : G.Walk v v} (hc : c.IsCircuit) (h : u c.support) :
                                                          (c.rotate h).IsCircuit
                                                          theorem SimpleGraph.Walk.IsCycle.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {c : G.Walk v v} (hc : c.IsCycle) (h : u c.support) :
                                                          (c.rotate h).IsCycle
                                                          theorem SimpleGraph.Walk.exists_boundary_dart {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (S : Set V) (uS : u S) (vS : vS) :
                                                          dp.darts, d.toProd.1 S d.toProd.2S

                                                          Given a set S and a walk w from u to v such that u ∈ S but v ∉ S, there exists a dart in the walk whose start is in S but whose end is not.

                                                          Type of paths #

                                                          @[reducible, inline]
                                                          abbrev SimpleGraph.Path {V : Type u} (G : SimpleGraph V) (u : V) (v : V) :

                                                          The type for paths between two vertices.

                                                          Equations
                                                          • G.Path u v = { p : G.Walk u v // p.IsPath }
                                                          Instances For
                                                            @[simp]
                                                            theorem SimpleGraph.Path.isPath {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path u v) :
                                                            (p).IsPath
                                                            @[simp]
                                                            theorem SimpleGraph.Path.isTrail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path u v) :
                                                            (p).IsTrail
                                                            @[simp]
                                                            theorem SimpleGraph.Path.nil_coe {V : Type u} {G : SimpleGraph V} {u : V} :
                                                            SimpleGraph.Path.nil = SimpleGraph.Walk.nil
                                                            def SimpleGraph.Path.nil {V : Type u} {G : SimpleGraph V} {u : V} :
                                                            G.Path u u

                                                            The length-0 path at a vertex.

                                                            Equations
                                                            • SimpleGraph.Path.nil = SimpleGraph.Walk.nil,
                                                            Instances For
                                                              @[simp]
                                                              theorem SimpleGraph.Path.singleton_coe {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) :
                                                              (SimpleGraph.Path.singleton h) = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
                                                              def SimpleGraph.Path.singleton {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) :
                                                              G.Path u v

                                                              The length-1 path between a pair of adjacent vertices.

                                                              Equations
                                                              Instances For
                                                                theorem SimpleGraph.Path.mk'_mem_edges_singleton {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) :
                                                                s(u, v) ((SimpleGraph.Path.singleton h)).edges
                                                                @[simp]
                                                                theorem SimpleGraph.Path.reverse_coe {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path u v) :
                                                                p.reverse = (p).reverse
                                                                def SimpleGraph.Path.reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path u v) :
                                                                G.Path v u

                                                                The reverse of a path is another path. See also SimpleGraph.Walk.reverse.

                                                                Equations
                                                                • p.reverse = (p).reverse,
                                                                Instances For
                                                                  theorem SimpleGraph.Path.count_support_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {p : G.Path u v} (hw : w (p).support) :
                                                                  List.count w (p).support = 1
                                                                  theorem SimpleGraph.Path.count_edges_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : G.Path u v} (e : Sym2 V) (hw : e (p).edges) :
                                                                  List.count e (p).edges = 1
                                                                  @[simp]
                                                                  theorem SimpleGraph.Path.nodup_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path u v) :
                                                                  (p).support.Nodup
                                                                  theorem SimpleGraph.Path.loop_eq {V : Type u} {G : SimpleGraph V} {v : V} (p : G.Path v v) :
                                                                  p = SimpleGraph.Path.nil
                                                                  theorem SimpleGraph.Path.not_mem_edges_of_loop {V : Type u} {G : SimpleGraph V} {v : V} {e : Sym2 V} {p : G.Path v v} :
                                                                  e(p).edges
                                                                  theorem SimpleGraph.Path.cons_isCycle {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path v u) (h : G.Adj u v) (he : s(u, v)(p).edges) :
                                                                  (SimpleGraph.Walk.cons h p).IsCycle

                                                                  Walks to paths #

                                                                  def SimpleGraph.Walk.bypass {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} :
                                                                  G.Walk u vG.Walk u v

                                                                  Given a walk, produces a walk from it by bypassing subwalks between repeated vertices. The result is a path, as shown in SimpleGraph.Walk.bypass_isPath. This is packaged up in SimpleGraph.Walk.toPath.

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem SimpleGraph.Walk.bypass_copy {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
                                                                    (p.copy hu hv).bypass = p.bypass.copy hu hv
                                                                    theorem SimpleGraph.Walk.bypass_isPath {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) :
                                                                    p.bypass.IsPath
                                                                    theorem SimpleGraph.Walk.length_bypass_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) :
                                                                    p.bypass.length p.length
                                                                    theorem SimpleGraph.Walk.bypass_eq_self_of_length_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) (h : p.length p.bypass.length) :
                                                                    p.bypass = p
                                                                    def SimpleGraph.Walk.toPath {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) :
                                                                    G.Path u v

                                                                    Given a walk, produces a path with the same endpoints using SimpleGraph.Walk.bypass.

                                                                    Equations
                                                                    • p.toPath = p.bypass,
                                                                    Instances For
                                                                      theorem SimpleGraph.Walk.support_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) :
                                                                      p.bypass.support p.support
                                                                      theorem SimpleGraph.Walk.support_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) :
                                                                      (p.toPath).support p.support
                                                                      theorem SimpleGraph.Walk.darts_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) :
                                                                      p.bypass.darts p.darts
                                                                      theorem SimpleGraph.Walk.edges_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) :
                                                                      p.bypass.edges p.edges
                                                                      theorem SimpleGraph.Walk.darts_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) :
                                                                      (p.toPath).darts p.darts
                                                                      theorem SimpleGraph.Walk.edges_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) :
                                                                      (p.toPath).edges p.edges

                                                                      Mapping paths #

                                                                      def SimpleGraph.Walk.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} :
                                                                      G.Walk u vG'.Walk (f u) (f v)

                                                                      Given a graph homomorphism, map walks to walks.

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.map_nil {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} :
                                                                        SimpleGraph.Walk.map f SimpleGraph.Walk.nil = SimpleGraph.Walk.nil
                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.map_cons {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) {w : V} (h : G.Adj w u) :
                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.map_copy {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
                                                                        SimpleGraph.Walk.map f (p.copy hu hv) = (SimpleGraph.Walk.map f p).copy
                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.map_id {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (p : G.Walk u v) :
                                                                        SimpleGraph.Walk.map SimpleGraph.Hom.id p = p
                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.map_map {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''} (f : G →g G') (f' : G' →g G'') {u : V} {v : V} (p : G.Walk u v) :
                                                                        theorem SimpleGraph.Walk.map_eq_of_eq {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u : V} {v : V} (p : G.Walk u v) {f : G →g G'} (f' : G →g G') (h : f = f') :

                                                                        Unlike categories, for graphs vertex equality is an important notion, so needing to be able to work with equality of graph homomorphisms is a necessary evil.

                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.map_eq_nil_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {p : G.Walk u u} :
                                                                        SimpleGraph.Walk.map f p = SimpleGraph.Walk.nil p = SimpleGraph.Walk.nil
                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.length_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) :
                                                                        (SimpleGraph.Walk.map f p).length = p.length
                                                                        theorem SimpleGraph.Walk.map_append {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.reverse_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) :
                                                                        (SimpleGraph.Walk.map f p).reverse = SimpleGraph.Walk.map f p.reverse
                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.support_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) :
                                                                        (SimpleGraph.Walk.map f p).support = List.map (f) p.support
                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.darts_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) :
                                                                        (SimpleGraph.Walk.map f p).darts = List.map f.mapDart p.darts
                                                                        @[simp]
                                                                        theorem SimpleGraph.Walk.edges_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) :
                                                                        (SimpleGraph.Walk.map f p).edges = List.map (Sym2.map f) p.edges
                                                                        theorem SimpleGraph.Walk.map_isPath_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : Function.Injective f) (hp : p.IsPath) :
                                                                        theorem SimpleGraph.Walk.IsPath.of_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u : V} {v : V} {p : G.Walk u v} {f : G →g G'} (hp : (SimpleGraph.Walk.map f p).IsPath) :
                                                                        p.IsPath
                                                                        theorem SimpleGraph.Walk.map_isPath_iff_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : Function.Injective f) :
                                                                        (SimpleGraph.Walk.map f p).IsPath p.IsPath
                                                                        theorem SimpleGraph.Walk.map_isTrail_iff_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : Function.Injective f) :
                                                                        (SimpleGraph.Walk.map f p).IsTrail p.IsTrail
                                                                        theorem SimpleGraph.Walk.map_isTrail_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : Function.Injective f) :
                                                                        p.IsTrail(SimpleGraph.Walk.map f p).IsTrail

                                                                        Alias of the reverse direction of SimpleGraph.Walk.map_isTrail_iff_of_injective.

                                                                        theorem SimpleGraph.Walk.map_isCycle_iff_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u} (hinj : Function.Injective f) :
                                                                        (SimpleGraph.Walk.map f p).IsCycle p.IsCycle
                                                                        theorem SimpleGraph.Walk.IsCycle.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u} (hinj : Function.Injective f) :
                                                                        p.IsCycle(SimpleGraph.Walk.map f p).IsCycle

                                                                        Alias of the reverse direction of SimpleGraph.Walk.map_isCycle_iff_of_injective.

                                                                        theorem SimpleGraph.Walk.map_injective_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} (hinj : Function.Injective f) (u : V) (v : V) :
                                                                        @[reducible, inline]
                                                                        abbrev SimpleGraph.Walk.mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {u : V} {v : V} (p : G.Walk u v) :
                                                                        G'.Walk u v

                                                                        The specialization of SimpleGraph.Walk.map for mapping walks to supergraphs.

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem SimpleGraph.Walk.mapLe_isTrail {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {u : V} {v : V} {p : G.Walk u v} :
                                                                          (SimpleGraph.Walk.mapLe h p).IsTrail p.IsTrail
                                                                          theorem SimpleGraph.Walk.IsTrail.mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {u : V} {v : V} {p : G.Walk u v} :
                                                                          p.IsTrail(SimpleGraph.Walk.mapLe h p).IsTrail

                                                                          Alias of the reverse direction of SimpleGraph.Walk.mapLe_isTrail.

                                                                          theorem SimpleGraph.Walk.IsTrail.of_mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {u : V} {v : V} {p : G.Walk u v} :
                                                                          (SimpleGraph.Walk.mapLe h p).IsTrailp.IsTrail

                                                                          Alias of the forward direction of SimpleGraph.Walk.mapLe_isTrail.

                                                                          @[simp]
                                                                          theorem SimpleGraph.Walk.mapLe_isPath {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {u : V} {v : V} {p : G.Walk u v} :
                                                                          (SimpleGraph.Walk.mapLe h p).IsPath p.IsPath
                                                                          theorem SimpleGraph.Walk.IsPath.of_mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {u : V} {v : V} {p : G.Walk u v} :
                                                                          (SimpleGraph.Walk.mapLe h p).IsPathp.IsPath

                                                                          Alias of the forward direction of SimpleGraph.Walk.mapLe_isPath.

                                                                          theorem SimpleGraph.Walk.IsPath.mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {u : V} {v : V} {p : G.Walk u v} :
                                                                          p.IsPath(SimpleGraph.Walk.mapLe h p).IsPath

                                                                          Alias of the reverse direction of SimpleGraph.Walk.mapLe_isPath.

                                                                          @[simp]
                                                                          theorem SimpleGraph.Walk.mapLe_isCycle {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {u : V} {p : G.Walk u u} :
                                                                          (SimpleGraph.Walk.mapLe h p).IsCycle p.IsCycle
                                                                          theorem SimpleGraph.Walk.IsCycle.mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {u : V} {p : G.Walk u u} :
                                                                          p.IsCycle(SimpleGraph.Walk.mapLe h p).IsCycle

                                                                          Alias of the reverse direction of SimpleGraph.Walk.mapLe_isCycle.

                                                                          theorem SimpleGraph.Walk.IsCycle.of_mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {u : V} {p : G.Walk u u} :
                                                                          (SimpleGraph.Walk.mapLe h p).IsCyclep.IsCycle

                                                                          Alias of the forward direction of SimpleGraph.Walk.mapLe_isCycle.

                                                                          @[simp]
                                                                          theorem SimpleGraph.Path.map_coe {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective f) {u : V} {v : V} (p : G.Path u v) :
                                                                          def SimpleGraph.Path.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective f) {u : V} {v : V} (p : G.Path u v) :
                                                                          G'.Path (f u) (f v)

                                                                          Given an injective graph homomorphism, map paths to paths.

                                                                          Equations
                                                                          Instances For
                                                                            theorem SimpleGraph.Path.map_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} (hinj : Function.Injective f) (u : V) (v : V) :
                                                                            @[simp]
                                                                            theorem SimpleGraph.Path.mapEmbedding_coe {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') {u : V} {v : V} (p : G.Path u v) :
                                                                            def SimpleGraph.Path.mapEmbedding {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') {u : V} {v : V} (p : G.Path u v) :
                                                                            G'.Path (f u) (f v)

                                                                            Given a graph embedding, map paths to paths.

                                                                            Equations
                                                                            Instances For

                                                                              ### Transferring between graphs

                                                                              def SimpleGraph.Walk.transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (H : SimpleGraph V) (h : ep.edges, e H.edgeSet) :
                                                                              H.Walk u v

                                                                              The walk p transferred to lie in H, given that H contains its edges.

                                                                              Equations
                                                                              Instances For
                                                                                theorem SimpleGraph.Walk.transfer_self {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                                                p.transfer G = p
                                                                                theorem SimpleGraph.Walk.transfer_eq_map_of_le {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ep.edges, e H.edgeSet) (GH : G H) :
                                                                                @[simp]
                                                                                theorem SimpleGraph.Walk.edges_transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ep.edges, e H.edgeSet) :
                                                                                (p.transfer H hp).edges = p.edges
                                                                                @[simp]
                                                                                theorem SimpleGraph.Walk.support_transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ep.edges, e H.edgeSet) :
                                                                                (p.transfer H hp).support = p.support
                                                                                @[simp]
                                                                                theorem SimpleGraph.Walk.length_transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ep.edges, e H.edgeSet) :
                                                                                (p.transfer H hp).length = p.length
                                                                                theorem SimpleGraph.Walk.IsPath.transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} {H : SimpleGraph V} (hp : ep.edges, e H.edgeSet) (pp : p.IsPath) :
                                                                                (p.transfer H hp).IsPath
                                                                                theorem SimpleGraph.Walk.IsCycle.transfer {V : Type u} {G : SimpleGraph V} {u : V} {H : SimpleGraph V} {q : G.Walk u u} (qc : q.IsCycle) (hq : eq.edges, e H.edgeSet) :
                                                                                (q.transfer H hq).IsCycle
                                                                                @[simp]
                                                                                theorem SimpleGraph.Walk.transfer_transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ep.edges, e H.edgeSet) {K : SimpleGraph V} (hp' : e(p.transfer H hp).edges, e K.edgeSet) :
                                                                                (p.transfer H hp).transfer K hp' = p.transfer K
                                                                                @[simp]
                                                                                theorem SimpleGraph.Walk.transfer_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} {w : V} (q : G.Walk v w) (hpq : e(p.append q).edges, e H.edgeSet) :
                                                                                (p.append q).transfer H hpq = (p.transfer H ).append (q.transfer H )
                                                                                @[simp]
                                                                                theorem SimpleGraph.Walk.reverse_transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ep.edges, e H.edgeSet) :
                                                                                (p.transfer H hp).reverse = p.reverse.transfer H

                                                                                Deleting edges #

                                                                                @[reducible, inline]
                                                                                abbrev SimpleGraph.Walk.toDeleteEdges {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v : V} {w : V} (p : G.Walk v w) (hp : ep.edges, es) :
                                                                                (G.deleteEdges s).Walk v w

                                                                                Given a walk that avoids a set of edges, produce a walk in the graph with those edges deleted.

                                                                                Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem SimpleGraph.Walk.toDeleteEdges_nil {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v : V} (hp : eSimpleGraph.Walk.nil.edges, es) :
                                                                                  SimpleGraph.Walk.toDeleteEdges s SimpleGraph.Walk.nil hp = SimpleGraph.Walk.nil
                                                                                  @[simp]
                                                                                  theorem SimpleGraph.Walk.toDeleteEdges_cons {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) (hp : e(SimpleGraph.Walk.cons h p).edges, es) :
                                                                                  @[reducible, inline]
                                                                                  abbrev SimpleGraph.Walk.toDeleteEdge {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (e : Sym2 V) (p : G.Walk v w) (hp : ep.edges) :
                                                                                  (G.deleteEdges {e}).Walk v w

                                                                                  Given a walk that avoids an edge, create a walk in the subgraph with that edge deleted. This is an abbreviation for SimpleGraph.Walk.toDeleteEdges.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem SimpleGraph.Walk.map_toDeleteEdges_eq {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (hp : ep.edges, es) :
                                                                                    theorem SimpleGraph.Walk.IsPath.toDeleteEdges {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (h : p.IsPath) (hp : ep.edges, es) :
                                                                                    theorem SimpleGraph.Walk.IsCycle.toDeleteEdges {V : Type u} {G : SimpleGraph V} {v : V} (s : Set (Sym2 V)) {p : G.Walk v v} (h : p.IsCycle) (hp : ep.edges, es) :
                                                                                    @[simp]
                                                                                    theorem SimpleGraph.Walk.toDeleteEdges_copy {V : Type u} {G : SimpleGraph V} {v : V} {u : V} {u' : V} {v' : V} (s : Set (Sym2 V)) (p : G.Walk u v) (hu : u = u') (hv : v = v') (h : e(p.copy hu hv).edges, es) :
                                                                                    SimpleGraph.Walk.toDeleteEdges s (p.copy hu hv) h = (SimpleGraph.Walk.toDeleteEdges s p ).copy hu hv

                                                                                    Reachable and Connected #

                                                                                    def SimpleGraph.Reachable {V : Type u} (G : SimpleGraph V) (u : V) (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_iff_nonempty_univ {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                                                                                      G.Reachable u v Set.univ.Nonempty
                                                                                      theorem SimpleGraph.Reachable.elim {V : Type u} {G : SimpleGraph V} {p : Prop} {u : V} {v : V} (h : G.Reachable u v) (hp : G.Walk u vp) :
                                                                                      p
                                                                                      theorem SimpleGraph.Reachable.elim_path {V : Type u} {G : SimpleGraph V} {p : Prop} {u : V} {v : V} (h : G.Reachable u v) (hp : G.Path u vp) :
                                                                                      p
                                                                                      theorem SimpleGraph.Walk.reachable {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                                                      G.Reachable u v
                                                                                      theorem SimpleGraph.Adj.reachable {V : Type u} {G : SimpleGraph V} {u : V} {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 : V} (huv : G.Reachable u v) :
                                                                                      G.Reachable v u
                                                                                      theorem SimpleGraph.reachable_comm {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                                                                                      G.Reachable u v G.Reachable v u
                                                                                      theorem SimpleGraph.Reachable.trans {V : Type u} {G : SimpleGraph V} {u : V} {v : 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 : V) :
                                                                                      G.Reachable u v Relation.ReflTransGen G.Adj u v
                                                                                      theorem SimpleGraph.Reachable.map {V : Type u} {V' : Type v} {u : V} {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 : V} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') (Guv : G.Reachable u v) :
                                                                                      G'.Reachable u v
                                                                                      theorem SimpleGraph.Iso.reachable_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {u : V} {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)

                                                                                      The equivalence relation on vertices given by SimpleGraph.Reachable.

                                                                                      Equations
                                                                                      • G.reachableSetoid = { r := G.Reachable, iseqv := }
                                                                                      Instances For

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

                                                                                        Equations
                                                                                        • G.Preconnected = ∀ (u v : V), G.Reachable u v
                                                                                        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) :
                                                                                          H.Preconnected
                                                                                          theorem SimpleGraph.Preconnected.mono {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') (hG : G.Preconnected) :
                                                                                          G'.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.connected_iff {V : Type u} (G : SimpleGraph V) :
                                                                                          G.Connected G.Preconnected Nonempty V
                                                                                          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.

                                                                                          • preconnected : G.Preconnected
                                                                                          • nonempty : Nonempty V
                                                                                          Instances For
                                                                                            theorem SimpleGraph.Connected.preconnected {V : Type u} {G : SimpleGraph V} (self : G.Connected) :
                                                                                            G.Preconnected
                                                                                            theorem SimpleGraph.Connected.nonempty {V : Type u} {G : SimpleGraph V} (self : G.Connected) :
                                                                                            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
                                                                                            Equations
                                                                                            • G.instCoeFunConnectedForallForallReachable = { coe := }
                                                                                            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 : SimpleGraph V} {G' : SimpleGraph V} (h : G G') (hG : G.Connected) :
                                                                                            G'.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

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

                                                                                            Equations
                                                                                            • G.ConnectedComponent = Quot G.Reachable
                                                                                            Instances For
                                                                                              def SimpleGraph.connectedComponentMk {V : Type u} (G : SimpleGraph V) (v : V) :
                                                                                              G.ConnectedComponent

                                                                                              Gives the connected component containing a particular vertex.

                                                                                              Equations
                                                                                              • G.connectedComponentMk v = Quot.mk G.Reachable v
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem SimpleGraph.ConnectedComponent.inhabited_default {V : Type u} {G : SimpleGraph V} [Inhabited V] :
                                                                                                default = G.connectedComponentMk default
                                                                                                instance SimpleGraph.ConnectedComponent.inhabited {V : Type u} {G : SimpleGraph V} [Inhabited V] :
                                                                                                Inhabited G.ConnectedComponent
                                                                                                Equations
                                                                                                • SimpleGraph.ConnectedComponent.inhabited = { default := G.connectedComponentMk default }
                                                                                                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 : G.ConnectedComponent) (d : G.ConnectedComponent) :
                                                                                                β c d
                                                                                                theorem SimpleGraph.ConnectedComponent.sound {V : Type u} {G : SimpleGraph V} {v : V} {w : V} :
                                                                                                G.Reachable v wG.connectedComponentMk v = G.connectedComponentMk w
                                                                                                theorem SimpleGraph.ConnectedComponent.exact {V : Type u} {G : SimpleGraph V} {v : V} {w : V} :
                                                                                                G.connectedComponentMk v = G.connectedComponentMk wG.Reachable v w
                                                                                                @[simp]
                                                                                                theorem SimpleGraph.ConnectedComponent.eq {V : Type u} {G : SimpleGraph V} {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 : 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.IsPathf v = f w) :
                                                                                                G.ConnectedComponentβ

                                                                                                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} :
                                                                                                  SimpleGraph.ConnectedComponent.lift f h (G.connectedComponentMk v) = f 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)
                                                                                                  theorem SimpleGraph.Preconnected.subsingleton_connectedComponent {V : Type u} {G : SimpleGraph V} (h : G.Preconnected) :
                                                                                                  Subsingleton G.ConnectedComponent
                                                                                                  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.

                                                                                                  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) :
                                                                                                    SimpleGraph.ConnectedComponent.map φ (G.connectedComponentMk v) = G'.connectedComponentMk (φ v)
                                                                                                    @[simp]
                                                                                                    theorem SimpleGraph.ConnectedComponent.map_id {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) :
                                                                                                    SimpleGraph.ConnectedComponent.map SimpleGraph.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'') :
                                                                                                    @[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) = SimpleGraph.ConnectedComponent.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' = SimpleGraph.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 = SimpleGraph.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 = SimpleGraph.ConnectedComponent.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.

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem SimpleGraph.Iso.connectedComponentEquiv_refl {V : Type u} {G : SimpleGraph V} :
                                                                                                      SimpleGraph.Iso.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'') :
                                                                                                      SimpleGraph.Iso.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.

                                                                                                      Equations
                                                                                                      • C.supp = {v : V | G.connectedComponentMk v = C}
                                                                                                      Instances For
                                                                                                        theorem SimpleGraph.ConnectedComponent.supp_injective {V : Type u} {G : SimpleGraph V} :
                                                                                                        Function.Injective SimpleGraph.ConnectedComponent.supp
                                                                                                        @[simp]
                                                                                                        theorem SimpleGraph.ConnectedComponent.supp_inj {V : Type u} {G : SimpleGraph V} {C : G.ConnectedComponent} {D : G.ConnectedComponent} :
                                                                                                        C.supp = D.supp C = D
                                                                                                        instance SimpleGraph.ConnectedComponent.instSetLike {V : Type u} {G : SimpleGraph V} :
                                                                                                        SetLike G.ConnectedComponent V
                                                                                                        Equations
                                                                                                        • SimpleGraph.ConnectedComponent.instSetLike = { coe := SimpleGraph.ConnectedComponent.supp, coe_injective' := }
                                                                                                        @[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.connectedComponentMk_mem {V : Type u} {G : SimpleGraph V} {v : V} :
                                                                                                        v G.connectedComponentMk v
                                                                                                        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.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          theorem SimpleGraph.Preconnected.set_univ_walk_nonempty {V : Type u} {G : SimpleGraph V} (hconn : G.Preconnected) (u : V) (v : V) :
                                                                                                          Set.univ.Nonempty
                                                                                                          theorem SimpleGraph.Connected.set_univ_walk_nonempty {V : Type u} {G : SimpleGraph V} (hconn : G.Connected) (u : V) (v : V) :
                                                                                                          Set.univ.Nonempty

                                                                                                          Walks as subgraphs #

                                                                                                          def SimpleGraph.Walk.toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                                                                                                          G.Walk u vG.Subgraph

                                                                                                          The subgraph consisting of the vertices and edges of the walk.

                                                                                                          Equations
                                                                                                          • SimpleGraph.Walk.nil.toSubgraph = G.singletonSubgraph u
                                                                                                          • (SimpleGraph.Walk.cons h q).toSubgraph = G.subgraphOfAdj h q.toSubgraph
                                                                                                          Instances For
                                                                                                            theorem SimpleGraph.Walk.toSubgraph_cons_nil_eq_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) :
                                                                                                            (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).toSubgraph = G.subgraphOfAdj h
                                                                                                            theorem SimpleGraph.Walk.mem_verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) :
                                                                                                            w p.toSubgraph.verts w p.support
                                                                                                            theorem SimpleGraph.Walk.start_mem_verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                                                                            u p.toSubgraph.verts
                                                                                                            theorem SimpleGraph.Walk.end_mem_verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                                                                            v p.toSubgraph.verts
                                                                                                            @[simp]
                                                                                                            theorem SimpleGraph.Walk.verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                                                                            p.toSubgraph.verts = {w : V | w p.support}
                                                                                                            theorem SimpleGraph.Walk.mem_edges_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {e : Sym2 V} :
                                                                                                            e p.toSubgraph.edgeSet e p.edges
                                                                                                            @[simp]
                                                                                                            theorem SimpleGraph.Walk.edgeSet_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                                                                            p.toSubgraph.edgeSet = {e : Sym2 V | e p.edges}
                                                                                                            @[simp]
                                                                                                            theorem SimpleGraph.Walk.toSubgraph_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
                                                                                                            (p.append q).toSubgraph = p.toSubgraph q.toSubgraph
                                                                                                            @[simp]
                                                                                                            theorem SimpleGraph.Walk.toSubgraph_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                                                                            p.reverse.toSubgraph = p.toSubgraph
                                                                                                            @[simp]
                                                                                                            theorem SimpleGraph.Walk.toSubgraph_rotate {V : Type u} {G : SimpleGraph V} {u : V} {v : V} [DecidableEq V] (c : G.Walk v v) (h : u c.support) :
                                                                                                            (c.rotate h).toSubgraph = c.toSubgraph
                                                                                                            @[simp]
                                                                                                            theorem SimpleGraph.Walk.toSubgraph_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u : V} {v : V} (f : G →g G') (p : G.Walk u v) :
                                                                                                            (SimpleGraph.Walk.map f p).toSubgraph = SimpleGraph.Subgraph.map f p.toSubgraph
                                                                                                            @[simp]
                                                                                                            theorem SimpleGraph.Walk.finite_neighborSet_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) :
                                                                                                            (p.toSubgraph.neighborSet w).Finite
                                                                                                            theorem SimpleGraph.Walk.toSubgraph_le_induce_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                                                                                            p.toSubgraph .induce {v_1 : V | v_1 p.support}

                                                                                                            Walks of a given length #

                                                                                                            theorem SimpleGraph.set_walk_self_length_zero_eq {V : Type u} {G : SimpleGraph V} (u : V) :
                                                                                                            {p : G.Walk u u | p.length = 0} = {SimpleGraph.Walk.nil}
                                                                                                            theorem SimpleGraph.set_walk_length_zero_eq_of_ne {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : u v) :
                                                                                                            {p : G.Walk u v | p.length = 0} =
                                                                                                            theorem SimpleGraph.set_walk_length_succ_eq {V : Type u} {G : SimpleGraph V} (u : V) (v : V) (n : ) :
                                                                                                            {p : G.Walk u v | p.length = n.succ} = ⋃ (w : V), ⋃ (h : G.Adj u w), SimpleGraph.Walk.cons h '' {p' : G.Walk w v | p'.length = n}
                                                                                                            @[simp]
                                                                                                            theorem SimpleGraph.walkLengthTwoEquivCommonNeighbors_symm_apply_coe {V : Type u} (G : SimpleGraph V) (u : V) (v : V) (w : (G.commonNeighbors u v)) :
                                                                                                            ((G.walkLengthTwoEquivCommonNeighbors u v).symm w) = (SimpleGraph.Adj.toWalk ).concat
                                                                                                            @[simp]
                                                                                                            theorem SimpleGraph.walkLengthTwoEquivCommonNeighbors_apply_coe {V : Type u} (G : SimpleGraph V) (u : V) (v : V) (p : { p : G.Walk u v // p.length = 2 }) :
                                                                                                            ((G.walkLengthTwoEquivCommonNeighbors u v) p) = (p).getVert 1
                                                                                                            def SimpleGraph.walkLengthTwoEquivCommonNeighbors {V : Type u} (G : SimpleGraph V) (u : V) (v : V) :
                                                                                                            { p : G.Walk u v // p.length = 2 } (G.commonNeighbors u v)

                                                                                                            Walks of length two from u to v correspond bijectively to common neighbours of u and v. Note that u and v may be the same.

                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              def SimpleGraph.finsetWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ) (u : V) (v : V) :
                                                                                                              Finset (G.Walk u v)

                                                                                                              The Finset of length-n walks from u to v. This is used to give {p : G.walk u v | p.length = n} a Fintype instance, and it can also be useful as a recursive description of this set when V is finite.

                                                                                                              See SimpleGraph.coe_finsetWalkLength_eq for the relationship between this Finset and the set of length-n walks.

                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              • G.finsetWalkLength 0 u v = if h : u = v then {SimpleGraph.Walk.nil} else
                                                                                                              Instances For
                                                                                                                theorem SimpleGraph.coe_finsetWalkLength_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ) (u : V) (v : V) :
                                                                                                                (G.finsetWalkLength n u v) = {p : G.Walk u v | p.length = n}
                                                                                                                theorem SimpleGraph.Walk.mem_finsetWalkLength_iff_length_eq {V : Type u} {G : SimpleGraph V} [DecidableEq V] [G.LocallyFinite] {n : } {u : V} {v : V} (p : G.Walk u v) :
                                                                                                                p G.finsetWalkLength n u v p.length = n
                                                                                                                instance SimpleGraph.fintypeSetWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u : V) (v : V) (n : ) :
                                                                                                                Fintype {p : G.Walk u v | p.length = n}
                                                                                                                Equations
                                                                                                                instance SimpleGraph.fintypeSubtypeWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u : V) (v : V) (n : ) :
                                                                                                                Fintype { p : G.Walk u v // p.length = n }
                                                                                                                Equations
                                                                                                                • G.fintypeSubtypeWalkLength u v n = G.fintypeSetWalkLength u v n
                                                                                                                theorem SimpleGraph.set_walk_length_toFinset_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ) (u : V) (v : V) :
                                                                                                                {p : G.Walk u v | p.length = n}.toFinset = G.finsetWalkLength n u v
                                                                                                                theorem SimpleGraph.card_set_walk_length_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u : V) (v : V) (n : ) :
                                                                                                                Fintype.card {p : G.Walk u v | p.length = n} = (G.finsetWalkLength n u v).card
                                                                                                                instance SimpleGraph.fintypeSetPathLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u : V) (v : V) (n : ) :
                                                                                                                Fintype {p : G.Walk u v | p.IsPath p.length = n}
                                                                                                                Equations
                                                                                                                theorem SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] (u : V) (v : V) :
                                                                                                                G.Reachable u v ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (n) u v).Nonempty
                                                                                                                Equations
                                                                                                                instance SimpleGraph.instFintypeConnectedComponent {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] :
                                                                                                                Fintype G.ConnectedComponent
                                                                                                                Equations
                                                                                                                instance SimpleGraph.instDecidablePreconnected {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] :
                                                                                                                Decidable G.Preconnected
                                                                                                                Equations
                                                                                                                instance SimpleGraph.instDecidableConnected {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] :
                                                                                                                Decidable G.Connected
                                                                                                                Equations
                                                                                                                • G.instDecidableConnected = .mpr (.mpr inferInstance)

                                                                                                                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 : V} :
                                                                                                                  G.IsBridge s(u, v) G.Adj u v ¬(G \ SimpleGraph.fromEdgeSet {s(u, v)}).Reachable u v
                                                                                                                  theorem SimpleGraph.reachable_delete_edges_iff_exists_walk {V : Type u} {G : SimpleGraph V} {v : V} {w : V} :
                                                                                                                  (G \ SimpleGraph.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 : 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} {v : 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 : V} {w : V} :
                                                                                                                  G.Adj v w (G \ SimpleGraph.fromEdgeSet {s(v, w)}).Reachable