Documentation

Mathlib.Combinatorics.SimpleGraph.Paths

Trail, Path, and Cycle #

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

Main definitions #

Tags #

trails, paths, circuits, cycles

Trails, paths, circuits, cycles #

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

A trail is a walk with no repeating edges.

Instances For
    theorem SimpleGraph.Walk.isTrail_def {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) :
    structure SimpleGraph.Walk.IsPath {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) extends p.IsTrail :

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

    Instances For
      theorem SimpleGraph.Walk.IsPath.isTrail {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.IsPath) :
      structure SimpleGraph.Walk.IsCircuit {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) extends p.IsTrail :

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

      Instances For
        theorem SimpleGraph.Walk.isCircuit_def {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) :
        theorem SimpleGraph.Walk.IsCircuit.isTrail {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (h : p.IsCircuit) :
        structure SimpleGraph.Walk.IsCycle {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) extends p.IsCircuit :

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

        Instances For
          theorem SimpleGraph.Walk.IsCycle.isCircuit {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (h : p.IsCycle) :
          @[simp]
          theorem SimpleGraph.Walk.isTrail_copy {V : Type u} {G : SimpleGraph V} {u v u' 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} {p : G.Walk u v} (h : p.support.Nodup) :
          theorem SimpleGraph.Walk.isPath_def {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) :
          @[simp]
          theorem SimpleGraph.Walk.isPath_copy {V : Type u} {G : SimpleGraph V} {u v u' 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 u' : V} (p : G.Walk u u) (hu : u = u') :
          theorem SimpleGraph.Walk.IsCircuit.not_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCircuit) :
          theorem SimpleGraph.Walk.isCycle_def {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) :
          @[simp]
          theorem SimpleGraph.Walk.isCycle_copy {V : Type u} {G : SimpleGraph V} {u 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) :
          @[simp]
          theorem SimpleGraph.Walk.IsTrail.of_cons {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w} :
          (cons h p).IsTrailp.IsTrail
          @[simp]
          theorem SimpleGraph.Walk.cons_isTrail_iff {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
          (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} (p : G.Walk u v) (h : p.IsTrail) :
          @[simp]
          theorem SimpleGraph.Walk.reverse_isTrail_iff {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) :
          theorem SimpleGraph.Walk.IsTrail.of_append_left {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) :
          theorem SimpleGraph.Walk.IsTrail.of_append_right {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) :
          theorem SimpleGraph.Walk.IsTrail.count_edges_le_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsTrail) (e : Sym2 V) :
          theorem SimpleGraph.Walk.IsTrail.count_edges_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsTrail) {e : Sym2 V} (he : e p.edges) :
          theorem SimpleGraph.Walk.IsPath.of_cons {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w} :
          (cons h p).IsPathp.IsPath
          @[simp]
          theorem SimpleGraph.Walk.cons_isPath_iff {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
          (cons h p).IsPath p.IsPath up.support
          theorem SimpleGraph.Walk.IsPath.cons {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk v w} (hp : p.IsPath) (hu : up.support) {h : G.Adj u v} :
          (cons h p).IsPath
          @[simp]
          theorem SimpleGraph.Walk.isPath_iff_eq_nil {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) :
          theorem SimpleGraph.Walk.IsPath.reverse {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.IsPath) :
          @[simp]
          theorem SimpleGraph.Walk.isPath_reverse_iff {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) :
          theorem SimpleGraph.Walk.IsPath.of_append_left {V : Type u} {G : SimpleGraph V} {u 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 w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsPath) :
          theorem SimpleGraph.Walk.IsPath.of_adj {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) :
          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) :
          theorem SimpleGraph.Walk.not_nil_of_isCycle_cons {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {h : G.Adj v u} (hc : (cons h p).IsCycle) :
          theorem SimpleGraph.Walk.cons_isCycle_iff {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk v u) (h : G.Adj u v) :
          (cons h p).IsCycle p.IsPath s(u, v)p.edges
          theorem SimpleGraph.Walk.IsCycle.reverse {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (h : p.IsCycle) :
          @[simp]
          theorem SimpleGraph.Walk.isCycle_reverse {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} :
          theorem SimpleGraph.Walk.IsCycle.isPath_of_append_right {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u} (h : ¬p.Nil) (hcyc : (p.append q).IsCycle) :
          theorem SimpleGraph.Walk.IsCycle.isPath_of_append_left {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u} (h : ¬q.Nil) (hcyc : (p.append q).IsCycle) :
          theorem SimpleGraph.Walk.IsPath.tail {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) :

          About paths #

          theorem SimpleGraph.Walk.IsPath.length_lt {V : Type u} {G : SimpleGraph V} [Fintype V] {u v : V} {p : G.Walk u v} (hp : p.IsPath) :
          theorem SimpleGraph.Walk.IsPath.getVert_injOn {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) :
          theorem SimpleGraph.Walk.IsPath.getVert_eq_start_iff {V : Type u} {G : SimpleGraph V} {u w : V} {i : } {p : G.Walk u w} (hp : p.IsPath) (hi : i p.length) :
          p.getVert i = u i = 0
          theorem SimpleGraph.Walk.IsPath.getVert_eq_end_iff {V : Type u} {G : SimpleGraph V} {u w : V} {i : } {p : G.Walk u w} (hp : p.IsPath) (hi : i p.length) :
          p.getVert i = w i = p.length

          About cycles #

          theorem SimpleGraph.Walk.IsCycle.getVert_injOn {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (hpc : p.IsCycle) :
          theorem SimpleGraph.Walk.IsCycle.getVert_injOn' {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (hpc : p.IsCycle) :
          theorem SimpleGraph.Walk.IsCycle.snd_ne_penultimate {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (hp : p.IsCycle) :
          theorem SimpleGraph.Walk.IsCycle.getVert_endpoint_iff {V : Type u} {G : SimpleGraph V} {u : V} {i : } {p : G.Walk u u} (hpc : p.IsCycle) (hl : i p.length) :
          p.getVert i = u i = 0 i = p.length
          theorem SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one {V : Type u} {G : SimpleGraph V} {u : V} {i : } {p : G.Walk u u} (hpc : p.IsCycle) (h : i p.length) :
          p.getVert (i - 1) p.getVert (i + 1)
          @[deprecated SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one (since := "2025-04-27")]
          theorem SimpleGraph.Walk.IsCycle.getVert_sub_one_neq_getVert_add_one {V : Type u} {G : SimpleGraph V} {u : V} {i : } {p : G.Walk u u} (hpc : p.IsCycle) (h : i p.length) :
          p.getVert (i - 1) p.getVert (i + 1)

          Alias of SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one.

          Walk decompositions #

          theorem SimpleGraph.Walk.IsTrail.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u p.support) :
          theorem SimpleGraph.Walk.IsTrail.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u p.support) :
          theorem SimpleGraph.Walk.IsPath.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u p.support) :
          theorem SimpleGraph.Walk.IsPath.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u p.support) :
          theorem SimpleGraph.Walk.IsTrail.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {c : G.Walk v v} (hc : c.IsTrail) (h : u c.support) :
          theorem SimpleGraph.Walk.IsCircuit.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {c : G.Walk v v} (hc : c.IsCircuit) (h : u c.support) :
          theorem SimpleGraph.Walk.IsCycle.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {c : G.Walk v v} (hc : c.IsCycle) (h : u c.support) :
          theorem SimpleGraph.Walk.IsCycle.isPath_takeUntil {V : Type u} {G : SimpleGraph V} {v w : V} [DecidableEq V] {c : G.Walk v v} (hc : c.IsCycle) (h : w c.support) :
          theorem SimpleGraph.Walk.endpoint_notMem_support_takeUntil {V : Type u} {G : SimpleGraph V} {u v w : V} [DecidableEq V] {p : G.Walk u v} (hp : p.IsPath) (hw : w p.support) (h : v w) :
          v(p.takeUntil w hw).support

          Taking a strict initial segment of a path removes the end vertex from the support.

          @[deprecated SimpleGraph.Walk.endpoint_notMem_support_takeUntil (since := "2025-05-23")]
          theorem SimpleGraph.Walk.endpoint_not_mem_support_takeUntil {V : Type u} {G : SimpleGraph V} {u v w : V} [DecidableEq V] {p : G.Walk u v} (hp : p.IsPath) (hw : w p.support) (h : v w) :
          v(p.takeUntil w hw).support

          Alias of SimpleGraph.Walk.endpoint_notMem_support_takeUntil.


          Taking a strict initial segment of a path removes the end vertex from the support.

          Type of paths #

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

          The type for paths between two vertices.

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

            The length-0 path at a vertex.

            Equations
            Instances For
              @[simp]
              theorem SimpleGraph.Path.nil_coe {V : Type u} {G : SimpleGraph V} {u : V} :
              def SimpleGraph.Path.singleton {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) :
              G.Path u v

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

              Equations
              Instances For
                @[simp]
                theorem SimpleGraph.Path.singleton_coe {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) :
                theorem SimpleGraph.Path.mk'_mem_edges_singleton {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) :
                s(u, v) (↑(singleton h)).edges
                def SimpleGraph.Path.reverse {V : Type u} {G : SimpleGraph V} {u 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
                Instances For
                  @[simp]
                  theorem SimpleGraph.Path.reverse_coe {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v) :
                  p.reverse = (↑p).reverse
                  theorem SimpleGraph.Path.count_support_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u 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} {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} (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) :
                  theorem SimpleGraph.Path.notMem_edges_of_loop {V : Type u} {G : SimpleGraph V} {v : V} {e : Sym2 V} {p : G.Path v v} :
                  e(↑p).edges
                  @[deprecated SimpleGraph.Path.notMem_edges_of_loop (since := "2025-05-23")]
                  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

                  Alias of SimpleGraph.Path.notMem_edges_of_loop.

                  theorem SimpleGraph.Path.cons_isCycle {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path v u) (h : G.Adj u v) (he : s(u, v)(↑p).edges) :

                  Walks to paths #

                  def SimpleGraph.Walk.bypass {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u 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 u' 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} (p : G.Walk u v) :
                    theorem SimpleGraph.Walk.length_bypass_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) :
                    theorem SimpleGraph.Walk.bypass_eq_self_of_length_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u 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} (p : G.Walk u v) :
                    G.Path u v

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

                    Equations
                    Instances For
                      theorem SimpleGraph.Walk.support_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) :
                      theorem SimpleGraph.Walk.darts_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) :
                      theorem SimpleGraph.Walk.edges_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) :
                      theorem SimpleGraph.Walk.darts_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) :
                      theorem SimpleGraph.Walk.edges_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) :

                      Mapping paths #

                      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} {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} {p : G.Walk u v} {f : G →g G'} (hp : (Walk.map f 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} {p : G.Walk u v} (hinj : Function.Injective f) :
                      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} {p : G.Walk u v} (hinj : Function.Injective f) :
                      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} {p : G.Walk u v} (hinj : Function.Injective f) :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                      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} (p : G.Path u v) :
                      G'.Path (f u) (f v)

                      Given an injective graph homomorphism, map paths to paths.

                      Equations
                      Instances For
                        @[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} (p : G.Path u v) :
                        (Path.map f hinj p) = Walk.map f p
                        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) :
                        def SimpleGraph.Path.mapEmbedding {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') {u v : V} (p : G.Path u v) :
                        G'.Path (f u) (f v)

                        Given a graph embedding, map paths to paths.

                        Equations
                        Instances For
                          @[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} (p : G.Path u v) :
                          theorem SimpleGraph.Path.mapEmbedding_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') (u v : V) :

                          Transferring between graphs #

                          theorem SimpleGraph.Walk.IsPath.transfer {V : Type u} {G : SimpleGraph V} {u v : V} {H : SimpleGraph V} {p : G.Walk u 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

                          Deleting edges #

                          theorem SimpleGraph.Walk.IsPath.toDeleteEdges {V : Type u} (G : SimpleGraph 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 u u' 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) :
                          toDeleteEdges s (p.copy hu hv) h = (toDeleteEdges s p ).copy hu hv