Documentation

Mathlib.Combinatorics.SimpleGraph.Walk

Walk #

In a simple graph, a walk is a finite sequence of adjacent vertices, and can be thought of equally well as a sequence of directed edges.

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 [Cho94].

Main definitions #

Tags #

walks

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))
                        theorem SimpleGraph.Walk.getVert_cons_one {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (q : G.Walk v w) (hadj : G.Adj u v) :
                        (SimpleGraph.Walk.cons hadj q).getVert 1 = v
                        @[simp]
                        theorem SimpleGraph.Walk.getVert_cons_succ {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {n : } (p : G.Walk v w) (h : G.Adj u v) :
                        (SimpleGraph.Walk.cons h p).getVert (n + 1) = p.getVert n
                        theorem SimpleGraph.Walk.getVert_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {n : } (p : G.Walk v w) (h : G.Adj u v) (hn : n 0) :
                        (SimpleGraph.Walk.cons h p).getVert n = p.getVert (n - 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.nil_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                        SimpleGraph.Walk.nil.append p = 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
                        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
                        theorem SimpleGraph.Walk.reverse_surjective {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                        Function.Surjective SimpleGraph.Walk.reverse
                        theorem SimpleGraph.Walk.reverse_injective {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                        Function.Injective SimpleGraph.Walk.reverse
                        theorem SimpleGraph.Walk.reverse_bijective {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                        Function.Bijective SimpleGraph.Walk.reverse
                        @[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 []
                                  @[simp]
                                  theorem SimpleGraph.Walk.head_support {V : Type u} {G : SimpleGraph V} {a : V} {b : V} (p : G.Walk a b) :
                                  p.support.head = a
                                  @[simp]
                                  theorem SimpleGraph.Walk.getLast_support {V : Type u} {G : SimpleGraph V} {a : V} {b : V} (p : G.Walk a b) :
                                  p.support.getLast = b
                                  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.head_darts_fst {V : Type u} {G : SimpleGraph V} {a : V} {b : V} (p : G.Walk a b) (hp : p.darts []) :
                                  (p.darts.head hp).toProd.1 = a
                                  @[simp]
                                  theorem SimpleGraph.Walk.getLast_darts_snd {V : Type u} {G : SimpleGraph V} {a : V} {b : V} (p : G.Walk a b) (hp : p.darts []) :
                                  (p.darts.getLast hp).toProd.2 = b
                                  @[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
                                  theorem SimpleGraph.Walk.edges_injective {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                                  Function.Injective SimpleGraph.Walk.edges
                                  theorem SimpleGraph.Walk.darts_injective {V : Type u} {G : SimpleGraph V} {u : V} {v : V} :
                                  Function.Injective SimpleGraph.Walk.darts
                                  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_lt_length {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} :
                                    ¬p.Nil 0 < p.length
                                    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
                                    Instances For
                                      @[simp]
                                      theorem SimpleGraph.Walk.notNilRec_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : 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) ) (h' : G.Adj u v) (q' : G.Walk v w) :
                                      SimpleGraph.Walk.notNilRec (fun {u v w : V} => cons) (SimpleGraph.Walk.cons h' q') = cons h' q'
                                      @[simp]
                                      theorem SimpleGraph.Walk.adj_getVert_one {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} (hp : ¬p.Nil) :
                                      G.Adj v (p.getVert 1)
                                      def SimpleGraph.Walk.drop {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (n : ) :
                                      G.Walk (p.getVert n) v

                                      The walk obtained by removing the first n darts of a walk.

                                      Equations
                                      • SimpleGraph.Walk.nil.drop n = SimpleGraph.Walk.nil
                                      • p.drop 0 = p.copy
                                      • (SimpleGraph.Walk.cons h q).drop n_2.succ = (q.drop n_2).copy
                                      Instances For
                                        def SimpleGraph.Walk.tail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) :
                                        G.Walk (p.getVert 1) v

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

                                        Equations
                                        • p.tail = p.drop 1
                                        Instances For
                                          @[simp]
                                          theorem SimpleGraph.Walk.tail_cons_nil {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) :
                                          (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).tail = SimpleGraph.Walk.nil
                                          theorem SimpleGraph.Walk.tail_cons_eq {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).tail = p.copy
                                          @[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.getVert 1)
                                          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.getVert 1), 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.getVert 1)
                                            theorem SimpleGraph.Walk.cons_tail_eq {V : Type u} {G : SimpleGraph V} {x : V} {y : V} (p : G.Walk x y) (hp : ¬p.Nil) :
                                            @[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.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.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.support = p.support.tail
                                            @[simp]
                                            theorem SimpleGraph.Walk.tail_cons {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} (p : G.Walk u v) (h : G.Adj t u) :
                                            (SimpleGraph.Walk.cons h p).tail = p.copy
                                            theorem SimpleGraph.Walk.support_tail_of_not_nil {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (hnp : ¬p.Nil) :
                                            p.tail.support = p.support.tail

                                            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
                                                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.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.

                                                  @[simp]
                                                  theorem SimpleGraph.Walk.getVert_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (i : ) (h : u = w) (h' : v = x) :
                                                  (p.copy h h').getVert i = p.getVert i
                                                  @[simp]
                                                  theorem SimpleGraph.Walk.getVert_tail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {n : } (p : G.Walk u v) (hnp : ¬p.Nil) :
                                                  p.tail.getVert n = p.getVert (n + 1)
                                                  @[irreducible]
                                                  theorem SimpleGraph.Walk.mem_support_iff_exists_getVert {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk v w} :
                                                  u p.support ∃ (n : ), p.getVert n = u n p.length

                                                  Given a walk w and a node in the support, there exists a natural n, such that given node is the n-th node (zero-indexed) in the walk. In addition, n is at most the length of the path. Due to the definition of getVert it would otherwise be legal to return a larger n for the last node.

                                                  Mapping walks #

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

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