Graph connectivity #
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.
-
A trail is a walk whose edges each appear no more than once.
-
A path is a trail whose vertices appear no more than once.
-
A cycle is a nonempty trail whose first and last vertices are the same and whose vertices except for the first appear no more than once.
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 #
-
SimpleGraph.Walk(with accompanying pattern definitionsSimpleGraph.Walk.nil'andSimpleGraph.Walk.cons') -
SimpleGraph.Walk.IsTrail,SimpleGraph.Walk.IsPath, andSimpleGraph.Walk.IsCycle. -
SimpleGraph.Walk.mapandSimpleGraph.Path.mapfor the induced map on walks, given an (injective) graph homomorphism. -
SimpleGraph.Reachablefor the relation of whether there exists a walk between a given pair of vertices -
SimpleGraph.PreconnectedandSimpleGraph.Connectedare predicates on simple graphs for whether every vertex can be reached from every other, and in the latter case, whether the vertex type is nonempty. -
SimpleGraph.ConnectedComponentis the type of connected components of a given graph. -
SimpleGraph.IsBridgefor whether an edge is a bridge edge
Main statements #
SimpleGraph.isBridge_iff_mem_and_forall_cycle_not_memcharacterizes bridge edges in terms of there being no cycle containing them.
Tags #
walks, trails, paths, circuits, cycles, bridge edges
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} → SimpleGraph.Walk G u u
- cons: {V : Type u} → {G : SimpleGraph V} → {u v w : V} → G.Adj u v → SimpleGraph.Walk G v w → SimpleGraph.Walk G u w
Instances For
instance
SimpleGraph.instDecidableEqWalk :
{V : Type u_1} → {G : SimpleGraph V} → {a a_1 : V} → [inst : DecidableEq V] → DecidableEq (SimpleGraph.Walk G 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 (SimpleGraph.Walk G v v)
Equations
- SimpleGraph.Walk.instInhabited G v = { default := SimpleGraph.Walk.nil }
@[match_pattern, reducible]
def
SimpleGraph.Adj.toWalk
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(h : G.Adj u v)
:
SimpleGraph.Walk G u v
The one-edge walk associated to a pair of adjacent vertices.
Equations
- SimpleGraph.Adj.toWalk h = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
Instances For
@[match_pattern, inline, reducible]
Pattern to get Walk.nil with the vertex as an explicit argument.
Equations
- SimpleGraph.Walk.nil' u = SimpleGraph.Walk.nil
Instances For
@[match_pattern, inline, reducible]
abbrev
SimpleGraph.Walk.cons'
{V : Type u}
{G : SimpleGraph V}
(u : V)
(v : V)
(w : V)
(h : G.Adj u v)
(p : SimpleGraph.Walk G v w)
:
SimpleGraph.Walk G u w
Pattern to get Walk.cons with the vertices as explicit arguments.
Equations
- SimpleGraph.Walk.cons' u v w h p = SimpleGraph.Walk.cons h p
Instances For
def
SimpleGraph.Walk.copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{u' : V}
{v' : V}
(p : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
:
SimpleGraph.Walk G 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
- SimpleGraph.Walk.copy p hu hv = hu ▸ hv ▸ p
Instances For
@[simp]
theorem
SimpleGraph.Walk.copy_rfl_rfl
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Walk.copy p (_ : u = u) (_ : v = v) = 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 : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
(hu' : u' = u'')
(hv' : v' = v'')
:
SimpleGraph.Walk.copy (SimpleGraph.Walk.copy p hu hv) hu' hv' = SimpleGraph.Walk.copy p (_ : u = u'') (_ : v = v'')
@[simp]
theorem
SimpleGraph.Walk.copy_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
{u' : V}
(hu : u = u')
:
SimpleGraph.Walk.copy SimpleGraph.Walk.nil 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 : SimpleGraph.Walk G v w)
(hu : u = u')
(hw : w = w')
:
SimpleGraph.Walk.copy (SimpleGraph.Walk.cons h p) hu hw = SimpleGraph.Walk.cons (_ : G.Adj u' v) (SimpleGraph.Walk.copy p (_ : v = v) 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 : SimpleGraph.Walk G v' w')
(hv : v' = v)
(hw : w' = w)
:
SimpleGraph.Walk.cons h (SimpleGraph.Walk.copy p hv hw) = SimpleGraph.Walk.copy (SimpleGraph.Walk.cons (_ : G.Adj u v') p) (_ : u = u) hw
theorem
SimpleGraph.Walk.exists_eq_cons_of_ne
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(hne : u ≠ v)
(p : SimpleGraph.Walk G u v)
:
∃ (w : V) (h : G.Adj u w) (p' : SimpleGraph.Walk G w v), p = SimpleGraph.Walk.cons h p'
def
SimpleGraph.Walk.length
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
SimpleGraph.Walk G u v → ℕ
The length of a walk is the number of edges/darts along it.
Equations
- SimpleGraph.Walk.length SimpleGraph.Walk.nil = 0
- SimpleGraph.Walk.length (SimpleGraph.Walk.cons h q) = Nat.succ (SimpleGraph.Walk.length q)
Instances For
def
SimpleGraph.Walk.append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
:
SimpleGraph.Walk G u v → SimpleGraph.Walk G v w → SimpleGraph.Walk G u w
The concatenation of two compatible walks.
Equations
- SimpleGraph.Walk.append SimpleGraph.Walk.nil q = q
- SimpleGraph.Walk.append (SimpleGraph.Walk.cons h p) x = SimpleGraph.Walk.cons h (SimpleGraph.Walk.append p x)
Instances For
def
SimpleGraph.Walk.concat
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(h : G.Adj v w)
:
SimpleGraph.Walk G u w
The reversed version of SimpleGraph.Walk.cons, concatenating an edge to
the end of a walk.
Equations
- SimpleGraph.Walk.concat p h = SimpleGraph.Walk.append p (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)
Instances For
theorem
SimpleGraph.Walk.concat_eq_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(h : G.Adj v w)
:
SimpleGraph.Walk.concat p h = SimpleGraph.Walk.append p (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)
def
SimpleGraph.Walk.reverseAux
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
:
SimpleGraph.Walk G u v → SimpleGraph.Walk G u w → SimpleGraph.Walk G v w
The concatenation of the reverse of the first walk with the second walk.
Equations
- SimpleGraph.Walk.reverseAux SimpleGraph.Walk.nil x = x
- SimpleGraph.Walk.reverseAux (SimpleGraph.Walk.cons h p) x = SimpleGraph.Walk.reverseAux p (SimpleGraph.Walk.cons (_ : G.Adj v_3 u) x)
Instances For
def
SimpleGraph.Walk.reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(w : SimpleGraph.Walk G u v)
:
SimpleGraph.Walk G v u
The walk in reverse.
Equations
- SimpleGraph.Walk.reverse w = SimpleGraph.Walk.reverseAux w SimpleGraph.Walk.nil
Instances For
def
SimpleGraph.Walk.getVert
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
SimpleGraph.Walk G u v → ℕ → V
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
- SimpleGraph.Walk.getVert SimpleGraph.Walk.nil x = u
- SimpleGraph.Walk.getVert (SimpleGraph.Walk.cons h p) 0 = u
- SimpleGraph.Walk.getVert (SimpleGraph.Walk.cons h q) (Nat.succ n) = SimpleGraph.Walk.getVert q n
Instances For
@[simp]
theorem
SimpleGraph.Walk.getVert_zero
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(w : SimpleGraph.Walk G u v)
:
SimpleGraph.Walk.getVert w 0 = u
theorem
SimpleGraph.Walk.getVert_of_length_le
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(w : SimpleGraph.Walk G u v)
{i : ℕ}
(hi : SimpleGraph.Walk.length w ≤ i)
:
SimpleGraph.Walk.getVert w i = v
@[simp]
theorem
SimpleGraph.Walk.getVert_length
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(w : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.adj_getVert_succ
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(w : SimpleGraph.Walk G u v)
{i : ℕ}
(hi : i < SimpleGraph.Walk.length w)
:
G.Adj (SimpleGraph.Walk.getVert w i) (SimpleGraph.Walk.getVert w (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 : SimpleGraph.Walk G v w)
(q : SimpleGraph.Walk G w x)
:
@[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 : SimpleGraph.Walk G v w)
:
SimpleGraph.Walk.append (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil) p = SimpleGraph.Walk.cons h p
@[simp]
theorem
SimpleGraph.Walk.append_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Walk.append p SimpleGraph.Walk.nil = p
@[simp]
theorem
SimpleGraph.Walk.nil_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Walk.append SimpleGraph.Walk.nil p = p
theorem
SimpleGraph.Walk.append_assoc
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{x : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G v w)
(r : SimpleGraph.Walk G w x)
:
@[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 : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G v w)
(hu : u = u')
(hv : v = v')
(hw : w = w')
:
SimpleGraph.Walk.append (SimpleGraph.Walk.copy p hu hv) (SimpleGraph.Walk.copy q hv hw) = SimpleGraph.Walk.copy (SimpleGraph.Walk.append p q) hu hw
theorem
SimpleGraph.Walk.concat_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(h : G.Adj u v)
:
SimpleGraph.Walk.concat SimpleGraph.Walk.nil 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 : SimpleGraph.Walk G v w)
(h' : G.Adj w x)
:
theorem
SimpleGraph.Walk.append_concat
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{x : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G v w)
(h : G.Adj w x)
:
theorem
SimpleGraph.Walk.concat_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{x : V}
(p : SimpleGraph.Walk G u v)
(h : G.Adj v w)
(q : SimpleGraph.Walk G w x)
:
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 : SimpleGraph.Walk G v w)
:
∃ (x : V) (q : SimpleGraph.Walk G u x) (h' : G.Adj x w), SimpleGraph.Walk.cons h p = SimpleGraph.Walk.concat q h'
theorem
SimpleGraph.Walk.exists_concat_eq_cons
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(h : G.Adj v w)
:
∃ (x : V) (h' : G.Adj u x) (q : SimpleGraph.Walk G x w), SimpleGraph.Walk.concat p h = SimpleGraph.Walk.cons h' q
@[simp]
theorem
SimpleGraph.Walk.reverse_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
SimpleGraph.Walk.reverse SimpleGraph.Walk.nil = 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.reverse (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil) = SimpleGraph.Walk.cons (_ : G.Adj v u) SimpleGraph.Walk.nil
@[simp]
theorem
SimpleGraph.Walk.cons_reverseAux
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{x : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G w x)
(h : G.Adj w u)
:
SimpleGraph.Walk.reverseAux (SimpleGraph.Walk.cons h p) q = SimpleGraph.Walk.reverseAux p (SimpleGraph.Walk.cons (_ : G.Adj u w) q)
@[simp]
theorem
SimpleGraph.Walk.append_reverseAux
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{x : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G v w)
(r : SimpleGraph.Walk G u x)
:
@[simp]
theorem
SimpleGraph.Walk.reverseAux_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{x : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G u w)
(r : SimpleGraph.Walk G w x)
:
theorem
SimpleGraph.Walk.reverseAux_eq_reverse_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G u w)
:
@[simp]
theorem
SimpleGraph.Walk.reverse_cons
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(h : G.Adj u v)
(p : SimpleGraph.Walk G v w)
:
SimpleGraph.Walk.reverse (SimpleGraph.Walk.cons h p) = SimpleGraph.Walk.append (SimpleGraph.Walk.reverse p) (SimpleGraph.Walk.cons (_ : G.Adj v u) SimpleGraph.Walk.nil)
@[simp]
theorem
SimpleGraph.Walk.reverse_copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{u' : V}
{v' : V}
(p : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
:
SimpleGraph.Walk.reverse (SimpleGraph.Walk.copy p hu hv) = SimpleGraph.Walk.copy (SimpleGraph.Walk.reverse p) hv hu
@[simp]
theorem
SimpleGraph.Walk.reverse_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G v w)
:
@[simp]
theorem
SimpleGraph.Walk.reverse_concat
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(h : G.Adj v w)
:
SimpleGraph.Walk.reverse (SimpleGraph.Walk.concat p h) = SimpleGraph.Walk.cons (_ : G.Adj w v) (SimpleGraph.Walk.reverse p)
@[simp]
theorem
SimpleGraph.Walk.reverse_reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.length_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
SimpleGraph.Walk.length SimpleGraph.Walk.nil = 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 : SimpleGraph.Walk G v w)
:
@[simp]
theorem
SimpleGraph.Walk.length_copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{u' : V}
{v' : V}
(p : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
:
@[simp]
theorem
SimpleGraph.Walk.length_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G v w)
:
@[simp]
theorem
SimpleGraph.Walk.length_concat
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(h : G.Adj v w)
:
@[simp]
theorem
SimpleGraph.Walk.length_reverseAux
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G u w)
:
@[simp]
theorem
SimpleGraph.Walk.length_reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.eq_of_length_eq_zero
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
:
SimpleGraph.Walk.length p = 0 → u = v
@[simp]
theorem
SimpleGraph.Walk.exists_length_eq_zero_iff
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
(∃ (p : SimpleGraph.Walk G u v), SimpleGraph.Walk.length p = 0) ↔ u = v
@[simp]
theorem
SimpleGraph.Walk.length_eq_zero_iff
{V : Type u}
{G : SimpleGraph V}
{u : V}
{p : SimpleGraph.Walk G u u}
:
SimpleGraph.Walk.length p = 0 ↔ p = SimpleGraph.Walk.nil
def
SimpleGraph.Walk.concatRecAux
{V : Type u}
{G : SimpleGraph V}
{motive : (u v : V) → SimpleGraph.Walk G u v → Sort u_1}
(Hnil : {u : V} → motive u u SimpleGraph.Walk.nil)
(Hconcat : {u v w : V} → (p : SimpleGraph.Walk G u v) → (h : G.Adj v w) → motive u v p → motive u w (SimpleGraph.Walk.concat p h))
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
motive v u (SimpleGraph.Walk.reverse p)
Auxiliary definition for SimpleGraph.Walk.concatRec
Equations
- One or more equations did not get rendered due to their size.
- SimpleGraph.Walk.concatRecAux Hnil Hconcat SimpleGraph.Walk.nil = Hnil
Instances For
def
SimpleGraph.Walk.concatRec
{V : Type u}
{G : SimpleGraph V}
{motive : (u v : V) → SimpleGraph.Walk G u v → Sort u_1}
(Hnil : {u : V} → motive u u SimpleGraph.Walk.nil)
(Hconcat : {u v w : V} → (p : SimpleGraph.Walk G u v) → (h : G.Adj v w) → motive u v p → motive u w (SimpleGraph.Walk.concat p h))
{u : V}
{v : V}
(p : SimpleGraph.Walk G 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
- SimpleGraph.Walk.concatRec Hnil Hconcat p = (_ : SimpleGraph.Walk.reverse (SimpleGraph.Walk.reverse p) = p) ▸ SimpleGraph.Walk.concatRecAux Hnil Hconcat (SimpleGraph.Walk.reverse p)
Instances For
@[simp]
theorem
SimpleGraph.Walk.concatRec_nil
{V : Type u}
{G : SimpleGraph V}
{motive : (u v : V) → SimpleGraph.Walk G u v → Sort u_1}
(Hnil : {u : V} → motive u u SimpleGraph.Walk.nil)
(Hconcat : {u v w : V} → (p : SimpleGraph.Walk G u v) → (h : G.Adj v w) → motive u v p → motive u w (SimpleGraph.Walk.concat p 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) → SimpleGraph.Walk G u v → Sort u_1}
(Hnil : {u : V} → motive u u SimpleGraph.Walk.nil)
(Hconcat : {u v w : V} → (p : SimpleGraph.Walk G u v) → (h : G.Adj v w) → motive u v p → motive u w (SimpleGraph.Walk.concat p h))
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(h : G.Adj v w)
:
SimpleGraph.Walk.concatRec Hnil Hconcat (SimpleGraph.Walk.concat p 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 : SimpleGraph.Walk G u v)
(h : G.Adj v u)
:
SimpleGraph.Walk.concat p h ≠ SimpleGraph.Walk.nil
theorem
SimpleGraph.Walk.concat_inj
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{v' : V}
{w : V}
{p : SimpleGraph.Walk G u v}
{h : G.Adj v w}
{p' : SimpleGraph.Walk G u v'}
{h' : G.Adj v' w}
(he : SimpleGraph.Walk.concat p h = SimpleGraph.Walk.concat p' h')
:
∃ (hv : v = v'), SimpleGraph.Walk.copy p (_ : u = u) hv = p'
def
SimpleGraph.Walk.support
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
SimpleGraph.Walk G u v → List V
The support of a walk is the list of vertices it visits in order.
Equations
- SimpleGraph.Walk.support SimpleGraph.Walk.nil = [u]
- SimpleGraph.Walk.support (SimpleGraph.Walk.cons h q) = u :: SimpleGraph.Walk.support q
Instances For
def
SimpleGraph.Walk.darts
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
SimpleGraph.Walk G u v → List (SimpleGraph.Dart G)
The darts of a walk is the list of darts it visits in order.
Equations
- SimpleGraph.Walk.darts SimpleGraph.Walk.nil = []
- SimpleGraph.Walk.darts (SimpleGraph.Walk.cons h q) = { toProd := (u, v_3), is_adj := h } :: SimpleGraph.Walk.darts q
Instances For
def
SimpleGraph.Walk.edges
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G 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
- SimpleGraph.Walk.edges p = List.map SimpleGraph.Dart.edge (SimpleGraph.Walk.darts p)
Instances For
@[simp]
theorem
SimpleGraph.Walk.support_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
SimpleGraph.Walk.support SimpleGraph.Walk.nil = [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 : SimpleGraph.Walk G v w)
:
@[simp]
theorem
SimpleGraph.Walk.support_concat
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(h : G.Adj v w)
:
@[simp]
theorem
SimpleGraph.Walk.support_copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{u' : V}
{v' : V}
(p : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
:
theorem
SimpleGraph.Walk.support_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(p' : SimpleGraph.Walk G v w)
:
@[simp]
theorem
SimpleGraph.Walk.support_reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.support_ne_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.tail_support_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(p' : SimpleGraph.Walk G v w)
:
theorem
SimpleGraph.Walk.support_eq_cons
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.start_mem_support
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.end_mem_support
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.support_nonempty
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
Set.Nonempty {w : V | w ∈ SimpleGraph.Walk.support p}
theorem
SimpleGraph.Walk.mem_support_iff
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
:
w ∈ SimpleGraph.Walk.support p ↔ w = u ∨ w ∈ List.tail (SimpleGraph.Walk.support p)
theorem
SimpleGraph.Walk.mem_support_nil_iff
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
u ∈ SimpleGraph.Walk.support SimpleGraph.Walk.nil ↔ 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 : SimpleGraph.Walk G u v)
(p' : SimpleGraph.Walk G v w)
:
t ∈ List.tail (SimpleGraph.Walk.support (SimpleGraph.Walk.append p p')) ↔ t ∈ List.tail (SimpleGraph.Walk.support p) ∨ t ∈ List.tail (SimpleGraph.Walk.support p')
@[simp]
theorem
SimpleGraph.Walk.end_mem_tail_support_of_ne
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(h : u ≠ v)
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.mem_support_append_iff
{V : Type u}
{G : SimpleGraph V}
{t : V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(p' : SimpleGraph.Walk G v w)
:
t ∈ SimpleGraph.Walk.support (SimpleGraph.Walk.append p p') ↔ t ∈ SimpleGraph.Walk.support p ∨ t ∈ SimpleGraph.Walk.support p'
@[simp]
theorem
SimpleGraph.Walk.subset_support_append_left
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G v w)
:
@[simp]
theorem
SimpleGraph.Walk.subset_support_append_right
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G v w)
:
theorem
SimpleGraph.Walk.coe_support
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
↑(SimpleGraph.Walk.support p) = {u} + ↑(List.tail (SimpleGraph.Walk.support p))
theorem
SimpleGraph.Walk.coe_support_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(p' : SimpleGraph.Walk G v w)
:
↑(SimpleGraph.Walk.support (SimpleGraph.Walk.append p p')) = {u} + ↑(List.tail (SimpleGraph.Walk.support p)) + ↑(List.tail (SimpleGraph.Walk.support p'))
theorem
SimpleGraph.Walk.coe_support_append'
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(p' : SimpleGraph.Walk G v w)
:
↑(SimpleGraph.Walk.support (SimpleGraph.Walk.append p p')) = ↑(SimpleGraph.Walk.support p) + ↑(SimpleGraph.Walk.support p') - {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 : SimpleGraph.Walk G v w)
:
List.Chain G.Adj u (SimpleGraph.Walk.support p)
theorem
SimpleGraph.Walk.chain'_adj_support
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
List.Chain' G.Adj (SimpleGraph.Walk.support p)
theorem
SimpleGraph.Walk.chain_dartAdj_darts
{V : Type u}
{G : SimpleGraph V}
{d : SimpleGraph.Dart G}
{v : V}
{w : V}
(h : d.toProd.2 = v)
(p : SimpleGraph.Walk G v w)
:
theorem
SimpleGraph.Walk.chain'_dartAdj_darts
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.edges_subset_edgeSet
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
⦃e : Sym2 V⦄
:
e ∈ SimpleGraph.Walk.edges p → e ∈ SimpleGraph.edgeSet G
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 : SimpleGraph.Walk G u v)
(h : s(x, y) ∈ SimpleGraph.Walk.edges p)
:
G.Adj x y
@[simp]
theorem
SimpleGraph.Walk.darts_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
SimpleGraph.Walk.darts SimpleGraph.Walk.nil = []
@[simp]
theorem
SimpleGraph.Walk.darts_cons
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(h : G.Adj u v)
(p : SimpleGraph.Walk G v w)
:
SimpleGraph.Walk.darts (SimpleGraph.Walk.cons h p) = { toProd := (u, v), is_adj := h } :: SimpleGraph.Walk.darts p
@[simp]
theorem
SimpleGraph.Walk.darts_concat
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(h : G.Adj v w)
:
SimpleGraph.Walk.darts (SimpleGraph.Walk.concat p h) = List.concat (SimpleGraph.Walk.darts p) { toProd := (v, w), is_adj := h }
@[simp]
theorem
SimpleGraph.Walk.darts_copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{u' : V}
{v' : V}
(p : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
:
@[simp]
theorem
SimpleGraph.Walk.darts_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(p' : SimpleGraph.Walk G v w)
:
@[simp]
theorem
SimpleGraph.Walk.darts_reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Walk.darts (SimpleGraph.Walk.reverse p) = List.reverse (List.map SimpleGraph.Dart.symm (SimpleGraph.Walk.darts p))
theorem
SimpleGraph.Walk.mem_darts_reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{d : SimpleGraph.Dart G}
{p : SimpleGraph.Walk G u v}
:
theorem
SimpleGraph.Walk.cons_map_snd_darts
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
u :: List.map (fun (x : SimpleGraph.Dart G) => x.toProd.2) (SimpleGraph.Walk.darts p) = SimpleGraph.Walk.support p
theorem
SimpleGraph.Walk.map_snd_darts
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
List.map (fun (x : SimpleGraph.Dart G) => x.toProd.2) (SimpleGraph.Walk.darts p) = List.tail (SimpleGraph.Walk.support p)
theorem
SimpleGraph.Walk.map_fst_darts_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
List.map (fun (x : SimpleGraph.Dart G) => x.toProd.1) (SimpleGraph.Walk.darts p) ++ [v] = SimpleGraph.Walk.support p
theorem
SimpleGraph.Walk.map_fst_darts
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
List.map (fun (x : SimpleGraph.Dart G) => x.toProd.1) (SimpleGraph.Walk.darts p) = List.dropLast (SimpleGraph.Walk.support p)
@[simp]
theorem
SimpleGraph.Walk.edges_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
SimpleGraph.Walk.edges SimpleGraph.Walk.nil = []
@[simp]
theorem
SimpleGraph.Walk.edges_cons
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(h : G.Adj u v)
(p : SimpleGraph.Walk G v w)
:
SimpleGraph.Walk.edges (SimpleGraph.Walk.cons h p) = s(u, v) :: SimpleGraph.Walk.edges p
@[simp]
theorem
SimpleGraph.Walk.edges_concat
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(h : G.Adj v w)
:
SimpleGraph.Walk.edges (SimpleGraph.Walk.concat p h) = List.concat (SimpleGraph.Walk.edges p) s(v, w)
@[simp]
theorem
SimpleGraph.Walk.edges_copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{u' : V}
{v' : V}
(p : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
:
@[simp]
theorem
SimpleGraph.Walk.edges_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(p' : SimpleGraph.Walk G v w)
:
@[simp]
theorem
SimpleGraph.Walk.edges_reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.length_support
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.length_darts
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.length_edges
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{d : SimpleGraph.Dart G}
:
d ∈ SimpleGraph.Walk.darts p → d.toProd.1 ∈ SimpleGraph.Walk.support p
theorem
SimpleGraph.Walk.dart_snd_mem_support_of_mem_darts
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{d : SimpleGraph.Dart G}
(h : d ∈ SimpleGraph.Walk.darts p)
:
d.toProd.2 ∈ SimpleGraph.Walk.support p
theorem
SimpleGraph.Walk.fst_mem_support_of_mem_edges
{V : Type u}
{G : SimpleGraph V}
{t : V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(he : s(t, u) ∈ SimpleGraph.Walk.edges p)
:
theorem
SimpleGraph.Walk.snd_mem_support_of_mem_edges
{V : Type u}
{G : SimpleGraph V}
{t : V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(he : s(t, u) ∈ SimpleGraph.Walk.edges p)
:
theorem
SimpleGraph.Walk.darts_nodup_of_support_nodup
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
(h : List.Nodup (SimpleGraph.Walk.support p))
:
theorem
SimpleGraph.Walk.edges_nodup_of_support_nodup
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
(h : List.Nodup (SimpleGraph.Walk.support p))
:
inductive
SimpleGraph.Walk.Nil
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
:
SimpleGraph.Walk G v w → Prop
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 SimpleGraph.Walk.nil
Instances For
@[simp]
theorem
SimpleGraph.Walk.nil_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
SimpleGraph.Walk.Nil SimpleGraph.Walk.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 : SimpleGraph.Walk G v w}
:
instance
SimpleGraph.Walk.instDecidableNil
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
:
Equations
- One or more equations did not get rendered due to their size.
theorem
SimpleGraph.Walk.Nil.eq
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G v w}
:
SimpleGraph.Walk.Nil p → v = w
theorem
SimpleGraph.Walk.not_nil_of_ne
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G v w}
:
v ≠ w → ¬SimpleGraph.Walk.Nil p
theorem
SimpleGraph.Walk.nil_iff_support_eq
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G v w}
:
theorem
SimpleGraph.Walk.nil_iff_length_eq
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G v w}
:
theorem
SimpleGraph.Walk.not_nil_iff
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G v w}
:
¬SimpleGraph.Walk.Nil p ↔ ∃ (u : V) (h : G.Adj v u) (q : SimpleGraph.Walk G u w), p = SimpleGraph.Walk.cons h q
def
SimpleGraph.Walk.notNilRec
{V : Type u}
{G : SimpleGraph V}
{u : V}
{w : V}
{motive : {u w : V} → (p : SimpleGraph.Walk G u w) → ¬SimpleGraph.Walk.Nil p → Sort u_1}
(cons : {u v w : V} →
(h : G.Adj u v) →
(q : SimpleGraph.Walk G v w) →
motive (SimpleGraph.Walk.cons h q) (_ : ¬SimpleGraph.Walk.Nil (SimpleGraph.Walk.cons h q)))
(p : SimpleGraph.Walk G u w)
(hp : ¬SimpleGraph.Walk.Nil p)
:
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 : SimpleGraph.Walk G v w)
(hp : ¬SimpleGraph.Walk.Nil p)
:
V
The second vertex along a non-nil walk.
Equations
- SimpleGraph.Walk.sndOfNotNil p hp = SimpleGraph.Walk.notNilRec (fun (x u x_1 : V) (x : G.Adj x u) (x : SimpleGraph.Walk G u x_1) => u) p hp
Instances For
@[simp]
theorem
SimpleGraph.Walk.adj_sndOfNotNil
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G v w}
(hp : ¬SimpleGraph.Walk.Nil p)
:
G.Adj v (SimpleGraph.Walk.sndOfNotNil p hp)
def
SimpleGraph.Walk.tail
{V : Type u}
{G : SimpleGraph V}
{x : V}
{y : V}
(p : SimpleGraph.Walk G x y)
(hp : ¬SimpleGraph.Walk.Nil p)
:
SimpleGraph.Walk G (SimpleGraph.Walk.sndOfNotNil p hp) y
The walk obtained by removing the first dart of a non-nil walk.
Equations
- SimpleGraph.Walk.tail p hp = SimpleGraph.Walk.notNilRec (fun {u v w : V} (x : G.Adj u v) (q : SimpleGraph.Walk G v w) => q) p hp
Instances For
@[simp]
theorem
SimpleGraph.Walk.firstDart_toProd
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(hp : ¬SimpleGraph.Walk.Nil p)
:
(SimpleGraph.Walk.firstDart p hp).toProd = (v, SimpleGraph.Walk.sndOfNotNil p hp)
def
SimpleGraph.Walk.firstDart
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(hp : ¬SimpleGraph.Walk.Nil p)
:
The first dart of a walk.
Equations
- SimpleGraph.Walk.firstDart p hp = { toProd := (v, SimpleGraph.Walk.sndOfNotNil p hp), is_adj := (_ : G.Adj v (SimpleGraph.Walk.sndOfNotNil p hp)) }
Instances For
theorem
SimpleGraph.Walk.edge_firstDart
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(hp : ¬SimpleGraph.Walk.Nil p)
:
SimpleGraph.Dart.edge (SimpleGraph.Walk.firstDart p hp) = s(v, SimpleGraph.Walk.sndOfNotNil p hp)
@[simp]
theorem
SimpleGraph.Walk.cons_tail_eq
{V : Type u}
{G : SimpleGraph V}
{x : V}
{y : V}
(p : SimpleGraph.Walk G x y)
(hp : ¬SimpleGraph.Walk.Nil p)
:
SimpleGraph.Walk.cons (_ : G.Adj x (SimpleGraph.Walk.sndOfNotNil p hp)) (SimpleGraph.Walk.tail p hp) = p
@[simp]
theorem
SimpleGraph.Walk.cons_support_tail
{V : Type u}
{G : SimpleGraph V}
{x : V}
{y : V}
(p : SimpleGraph.Walk G x y)
(hp : ¬SimpleGraph.Walk.Nil p)
:
@[simp]
theorem
SimpleGraph.Walk.length_tail_add_one
{V : Type u}
{G : SimpleGraph V}
{x : V}
{y : V}
{p : SimpleGraph.Walk G x y}
(hp : ¬SimpleGraph.Walk.Nil p)
:
@[simp]
theorem
SimpleGraph.Walk.nil_copy
{V : Type u}
{G : SimpleGraph V}
{x : V}
{y : V}
{x' : V}
{y' : V}
{p : SimpleGraph.Walk G x y}
(hx : x = x')
(hy : y = y')
:
Trails, paths, circuits, cycles #
theorem
SimpleGraph.Walk.isTrail_def
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
structure
SimpleGraph.Walk.IsTrail
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
A trail is a walk with no repeating edges.
- edges_nodup : List.Nodup (SimpleGraph.Walk.edges p)
Instances For
structure
SimpleGraph.Walk.IsPath
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
extends
SimpleGraph.Walk.IsTrail
:
A path is a walk with no repeating vertices.
Use simple_graph.walk.is_path.mk' for a simpler constructor.
- edges_nodup : List.Nodup (SimpleGraph.Walk.edges p)
- support_nodup : List.Nodup (SimpleGraph.Walk.support p)
Instances For
theorem
SimpleGraph.Walk.IsPath.isTrail :
∀ {V : Type u_1} {G : SimpleGraph V} {a a_1 : V} {p : SimpleGraph.Walk G a a_1},
SimpleGraph.Walk.IsPath p → SimpleGraph.Walk.IsTrail p
theorem
SimpleGraph.Walk.isCircuit_def
{V : Type u}
{G : SimpleGraph V}
{u : V}
(p : SimpleGraph.Walk G u u)
:
SimpleGraph.Walk.IsCircuit p ↔ SimpleGraph.Walk.IsTrail p ∧ p ≠ SimpleGraph.Walk.nil
structure
SimpleGraph.Walk.IsCircuit
{V : Type u}
{G : SimpleGraph V}
{u : V}
(p : SimpleGraph.Walk G u u)
extends
SimpleGraph.Walk.IsTrail
:
A circuit at u : V is a nonempty trail beginning and ending at u.
- edges_nodup : List.Nodup (SimpleGraph.Walk.edges p)
- ne_nil : p ≠ SimpleGraph.Walk.nil
Instances For
theorem
SimpleGraph.Walk.IsCircuit.isTrail :
∀ {V : Type u_1} {G : SimpleGraph V} {a : V} {p : SimpleGraph.Walk G a a},
SimpleGraph.Walk.IsCircuit p → SimpleGraph.Walk.IsTrail p
structure
SimpleGraph.Walk.IsCycle
{V : Type u}
{G : SimpleGraph V}
{u : V}
(p : SimpleGraph.Walk G 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 : List.Nodup (SimpleGraph.Walk.edges p)
- ne_nil : p ≠ SimpleGraph.Walk.nil
- support_nodup : List.Nodup (List.tail (SimpleGraph.Walk.support p))
Instances For
theorem
SimpleGraph.Walk.IsCycle.isCircuit :
∀ {V : Type u_1} {G : SimpleGraph V} {a : V} {p : SimpleGraph.Walk G a a},
SimpleGraph.Walk.IsCycle p → SimpleGraph.Walk.IsCircuit p
@[simp]
theorem
SimpleGraph.Walk.isTrail_copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{u' : V}
{v' : V}
(p : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
:
theorem
SimpleGraph.Walk.IsPath.mk'
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
(h : List.Nodup (SimpleGraph.Walk.support p))
:
theorem
SimpleGraph.Walk.isPath_def
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.isPath_copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{u' : V}
{v' : V}
(p : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
:
@[simp]
theorem
SimpleGraph.Walk.isCircuit_copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{u' : V}
(p : SimpleGraph.Walk G u u)
(hu : u = u')
:
theorem
SimpleGraph.Walk.isCycle_def
{V : Type u}
{G : SimpleGraph V}
{u : V}
(p : SimpleGraph.Walk G u u)
:
SimpleGraph.Walk.IsCycle p ↔ SimpleGraph.Walk.IsTrail p ∧ p ≠ SimpleGraph.Walk.nil ∧ List.Nodup (List.tail (SimpleGraph.Walk.support p))
@[simp]
theorem
SimpleGraph.Walk.isCycle_copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{u' : V}
(p : SimpleGraph.Walk G u u)
(hu : u = u')
:
@[simp]
theorem
SimpleGraph.Walk.IsTrail.nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
SimpleGraph.Walk.IsTrail SimpleGraph.Walk.nil
theorem
SimpleGraph.Walk.IsTrail.of_cons
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{h : G.Adj u v}
{p : SimpleGraph.Walk G v w}
:
@[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 : SimpleGraph.Walk G v w)
:
SimpleGraph.Walk.IsTrail (SimpleGraph.Walk.cons h p) ↔ SimpleGraph.Walk.IsTrail p ∧ s(u, v) ∉ SimpleGraph.Walk.edges p
theorem
SimpleGraph.Walk.IsTrail.reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
(h : SimpleGraph.Walk.IsTrail p)
:
@[simp]
theorem
SimpleGraph.Walk.reverse_isTrail_iff
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.IsTrail.of_append_left
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G u v}
{q : SimpleGraph.Walk G v w}
(h : SimpleGraph.Walk.IsTrail (SimpleGraph.Walk.append p q))
:
theorem
SimpleGraph.Walk.IsTrail.of_append_right
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G u v}
{q : SimpleGraph.Walk G v w}
(h : SimpleGraph.Walk.IsTrail (SimpleGraph.Walk.append p q))
:
theorem
SimpleGraph.Walk.IsTrail.count_edges_le_one
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
(h : SimpleGraph.Walk.IsTrail p)
(e : Sym2 V)
:
List.count e (SimpleGraph.Walk.edges p) ≤ 1
theorem
SimpleGraph.Walk.IsTrail.count_edges_eq_one
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
(h : SimpleGraph.Walk.IsTrail p)
{e : Sym2 V}
(he : e ∈ SimpleGraph.Walk.edges p)
:
List.count e (SimpleGraph.Walk.edges p) = 1
theorem
SimpleGraph.Walk.IsPath.nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
SimpleGraph.Walk.IsPath SimpleGraph.Walk.nil
theorem
SimpleGraph.Walk.IsPath.of_cons
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{h : G.Adj u v}
{p : SimpleGraph.Walk G v w}
:
@[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 : SimpleGraph.Walk G v w)
:
theorem
SimpleGraph.Walk.IsPath.cons
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
∀ {a : V} {p : SimpleGraph.Walk G v a},
SimpleGraph.Walk.IsPath p →
u ∉ SimpleGraph.Walk.support p → ∀ {h : G.Adj u v}, SimpleGraph.Walk.IsPath (SimpleGraph.Walk.cons h p)
@[simp]
theorem
SimpleGraph.Walk.isPath_iff_eq_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
(p : SimpleGraph.Walk G u u)
:
SimpleGraph.Walk.IsPath p ↔ p = SimpleGraph.Walk.nil
theorem
SimpleGraph.Walk.IsPath.reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
(h : SimpleGraph.Walk.IsPath p)
:
@[simp]
theorem
SimpleGraph.Walk.isPath_reverse_iff
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.IsPath.of_append_left
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G u v}
{q : SimpleGraph.Walk G v w}
:
theorem
SimpleGraph.Walk.IsPath.of_append_right
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G u v}
{q : SimpleGraph.Walk G v w}
(h : SimpleGraph.Walk.IsPath (SimpleGraph.Walk.append p q))
:
@[simp]
theorem
SimpleGraph.Walk.IsCycle.not_of_nil
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
¬SimpleGraph.Walk.IsCycle SimpleGraph.Walk.nil
theorem
SimpleGraph.Walk.IsCycle.ne_bot
{V : Type u}
{G : SimpleGraph V}
{u : V}
{p : SimpleGraph.Walk G u u}
:
SimpleGraph.Walk.IsCycle p → G ≠ ⊥
theorem
SimpleGraph.Walk.cons_isCycle_iff
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G v u)
(h : G.Adj u v)
:
SimpleGraph.Walk.IsCycle (SimpleGraph.Walk.cons h p) ↔ SimpleGraph.Walk.IsPath p ∧ s(u, v) ∉ SimpleGraph.Walk.edges p
theorem
SimpleGraph.Walk.IsPath.tail
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
(hp : SimpleGraph.Walk.IsPath p)
(hp' : ¬SimpleGraph.Walk.Nil p)
:
About paths #
instance
SimpleGraph.Walk.instDecidableIsPath
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
Equations
- SimpleGraph.Walk.instDecidableIsPath p = Eq.mpr (_ : Decidable (SimpleGraph.Walk.IsPath p) = Decidable (List.Nodup (SimpleGraph.Walk.support p))) inferInstance
theorem
SimpleGraph.Walk.IsPath.length_lt
{V : Type u}
{G : SimpleGraph V}
[Fintype V]
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
(hp : SimpleGraph.Walk.IsPath p)
:
Walk decompositions #
def
SimpleGraph.Walk.takeUntil
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(u : V)
:
u ∈ SimpleGraph.Walk.support p → SimpleGraph.Walk G 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.takeUntil SimpleGraph.Walk.nil x x_1 = Eq.mpr (_ : SimpleGraph.Walk G v x = SimpleGraph.Walk G v v) SimpleGraph.Walk.nil
Instances For
def
SimpleGraph.Walk.dropUntil
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(u : V)
:
u ∈ SimpleGraph.Walk.support p → SimpleGraph.Walk G 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.dropUntil SimpleGraph.Walk.nil x x_1 = Eq.mpr (_ : SimpleGraph.Walk G x v = SimpleGraph.Walk G v v) 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 : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
:
SimpleGraph.Walk.append (SimpleGraph.Walk.takeUntil p u h) (SimpleGraph.Walk.dropUntil p 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 : SimpleGraph.Walk G u v}
:
w ∈ SimpleGraph.Walk.support p ↔ ∃ (q : SimpleGraph.Walk G u w) (r : SimpleGraph.Walk G w v), p = SimpleGraph.Walk.append q 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 : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
:
List.count u (SimpleGraph.Walk.support (SimpleGraph.Walk.takeUntil p u h)) = 1
theorem
SimpleGraph.Walk.count_edges_takeUntil_le_one
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
(x : V)
:
List.count s(u, x) (SimpleGraph.Walk.edges (SimpleGraph.Walk.takeUntil p u h)) ≤ 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 : SimpleGraph.Walk G v w)
(hv : v = v')
(hw : w = w')
(h : u ∈ SimpleGraph.Walk.support (SimpleGraph.Walk.copy p hv hw))
:
SimpleGraph.Walk.takeUntil (SimpleGraph.Walk.copy p hv hw) u h = SimpleGraph.Walk.copy (SimpleGraph.Walk.takeUntil p u (_ : u ∈ SimpleGraph.Walk.support p)) hv (_ : u = u)
@[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 : SimpleGraph.Walk G v w)
(hv : v = v')
(hw : w = w')
(h : u ∈ SimpleGraph.Walk.support (SimpleGraph.Walk.copy p hv hw))
:
SimpleGraph.Walk.dropUntil (SimpleGraph.Walk.copy p hv hw) u h = SimpleGraph.Walk.copy (SimpleGraph.Walk.dropUntil p u (_ : u ∈ SimpleGraph.Walk.support p)) (_ : u = u) hw
theorem
SimpleGraph.Walk.support_takeUntil_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.support_dropUntil_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.darts_takeUntil_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.darts_dropUntil_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.edges_takeUntil_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.edges_dropUntil_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.length_takeUntil_le
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.length_dropUntil_le
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.IsTrail.takeUntil
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G v w}
(hc : SimpleGraph.Walk.IsTrail p)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.IsTrail.dropUntil
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G v w}
(hc : SimpleGraph.Walk.IsTrail p)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.IsPath.takeUntil
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G v w}
(hc : SimpleGraph.Walk.IsPath p)
(h : u ∈ SimpleGraph.Walk.support p)
:
theorem
SimpleGraph.Walk.IsPath.dropUntil
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
{p : SimpleGraph.Walk G v w}
(hc : SimpleGraph.Walk.IsPath p)
(h : u ∈ SimpleGraph.Walk.support p)
:
def
SimpleGraph.Walk.rotate
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(c : SimpleGraph.Walk G v v)
(h : u ∈ SimpleGraph.Walk.support c)
:
SimpleGraph.Walk G u u
Rotate a loop walk such that it is centered at the given vertex.
Equations
Instances For
@[simp]
theorem
SimpleGraph.Walk.support_rotate
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(c : SimpleGraph.Walk G v v)
(h : u ∈ SimpleGraph.Walk.support c)
:
theorem
SimpleGraph.Walk.rotate_darts
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(c : SimpleGraph.Walk G v v)
(h : u ∈ SimpleGraph.Walk.support c)
:
theorem
SimpleGraph.Walk.rotate_edges
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(c : SimpleGraph.Walk G v v)
(h : u ∈ SimpleGraph.Walk.support c)
:
theorem
SimpleGraph.Walk.IsTrail.rotate
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{c : SimpleGraph.Walk G v v}
(hc : SimpleGraph.Walk.IsTrail c)
(h : u ∈ SimpleGraph.Walk.support c)
:
theorem
SimpleGraph.Walk.IsCircuit.rotate
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{c : SimpleGraph.Walk G v v}
(hc : SimpleGraph.Walk.IsCircuit c)
(h : u ∈ SimpleGraph.Walk.support c)
:
theorem
SimpleGraph.Walk.IsCycle.rotate
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{c : SimpleGraph.Walk G v v}
(hc : SimpleGraph.Walk.IsCycle c)
(h : u ∈ SimpleGraph.Walk.support c)
:
theorem
SimpleGraph.Walk.exists_boundary_dart
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
(S : Set V)
(uS : u ∈ S)
(vS : v ∉ S)
:
∃ d ∈ SimpleGraph.Walk.darts p, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
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 #
@[inline, reducible]
The type for paths between two vertices.
Equations
- SimpleGraph.Path G u v = { p : SimpleGraph.Walk G u v // SimpleGraph.Walk.IsPath p }
Instances For
@[simp]
theorem
SimpleGraph.Path.isPath
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Path G u v)
:
@[simp]
theorem
SimpleGraph.Path.isTrail
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Path G u v)
:
@[simp]
theorem
SimpleGraph.Path.nil_coe
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
↑SimpleGraph.Path.nil = SimpleGraph.Walk.nil
The length-0 path at a vertex.
Equations
- SimpleGraph.Path.nil = { val := SimpleGraph.Walk.nil, property := (_ : SimpleGraph.Walk.IsPath 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)
:
SimpleGraph.Path G u v
The length-1 path between a pair of adjacent vertices.
Equations
- SimpleGraph.Path.singleton h = { val := SimpleGraph.Walk.cons h SimpleGraph.Walk.nil, property := (_ : SimpleGraph.Walk.IsPath (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)) }
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.Walk.edges ↑(SimpleGraph.Path.singleton h)
@[simp]
theorem
SimpleGraph.Path.reverse_coe
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Path G u v)
:
def
SimpleGraph.Path.reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Path G u v)
:
SimpleGraph.Path G v u
The reverse of a path is another path. See also SimpleGraph.Walk.reverse.
Equations
- SimpleGraph.Path.reverse p = { val := SimpleGraph.Walk.reverse ↑p, property := (_ : SimpleGraph.Walk.IsPath (SimpleGraph.Walk.reverse ↑p)) }
Instances For
theorem
SimpleGraph.Path.count_support_eq_one
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
{p : SimpleGraph.Path G u v}
(hw : w ∈ SimpleGraph.Walk.support ↑p)
:
List.count w (SimpleGraph.Walk.support ↑p) = 1
theorem
SimpleGraph.Path.count_edges_eq_one
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{p : SimpleGraph.Path G u v}
(e : Sym2 V)
(hw : e ∈ SimpleGraph.Walk.edges ↑p)
:
List.count e (SimpleGraph.Walk.edges ↑p) = 1
@[simp]
theorem
SimpleGraph.Path.nodup_support
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Path G u v)
:
theorem
SimpleGraph.Path.loop_eq
{V : Type u}
{G : SimpleGraph V}
{v : V}
(p : SimpleGraph.Path G 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 : SimpleGraph.Path G v v}
:
e ∉ SimpleGraph.Walk.edges ↑p
theorem
SimpleGraph.Path.cons_isCycle
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Path G v u)
(h : G.Adj u v)
(he : s(u, v) ∉ SimpleGraph.Walk.edges ↑p)
:
Walks to paths #
def
SimpleGraph.Walk.bypass
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
:
SimpleGraph.Walk G u v → SimpleGraph.Walk G 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
- One or more equations did not get rendered due to their size.
- SimpleGraph.Walk.bypass SimpleGraph.Walk.nil = SimpleGraph.Walk.nil
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 : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
:
SimpleGraph.Walk.bypass (SimpleGraph.Walk.copy p hu hv) = SimpleGraph.Walk.copy (SimpleGraph.Walk.bypass p) hu hv
theorem
SimpleGraph.Walk.bypass_isPath
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.length_bypass_le
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
def
SimpleGraph.Walk.toPath
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Path G u v
Given a walk, produces a path with the same endpoints using SimpleGraph.Walk.bypass.
Equations
- SimpleGraph.Walk.toPath p = { val := SimpleGraph.Walk.bypass p, property := (_ : SimpleGraph.Walk.IsPath (SimpleGraph.Walk.bypass p)) }
Instances For
theorem
SimpleGraph.Walk.support_bypass_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.support_toPath_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.darts_bypass_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.edges_bypass_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.darts_toPath_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.edges_toPath_subset
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
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}
:
SimpleGraph.Walk G u v → SimpleGraph.Walk G' (f u) (f v)
Given a graph homomorphism, map walks to walks.
Equations
- SimpleGraph.Walk.map f SimpleGraph.Walk.nil = SimpleGraph.Walk.nil
- SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h q) = SimpleGraph.Walk.cons (_ : G'.Adj (f u) (f v_3)) (SimpleGraph.Walk.map f q)
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 : SimpleGraph.Walk G u v)
{w : V}
(h : G.Adj w u)
:
SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h p) = SimpleGraph.Walk.cons (_ : G'.Adj (f w) (f u)) (SimpleGraph.Walk.map f p)
@[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 : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
:
SimpleGraph.Walk.map f (SimpleGraph.Walk.copy p hu hv) = SimpleGraph.Walk.copy (SimpleGraph.Walk.map f p) (_ : f u = f u') (_ : f v = f v')
@[simp]
theorem
SimpleGraph.Walk.map_id
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
(p : SimpleGraph.Walk G 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 : SimpleGraph.Walk G u v)
:
SimpleGraph.Walk.map f' (SimpleGraph.Walk.map f p) = SimpleGraph.Walk.map (SimpleGraph.Hom.comp f' f) p
theorem
SimpleGraph.Walk.map_eq_of_eq
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{f : G →g G'}
(f' : G →g G')
(h : f = f')
:
SimpleGraph.Walk.map f p = SimpleGraph.Walk.copy (SimpleGraph.Walk.map f' p) (_ : f' u = f u) (_ : f' v = f v)
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 : SimpleGraph.Walk G 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 : SimpleGraph.Walk G u v)
:
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 : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G 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 : SimpleGraph.Walk G u v)
:
@[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 : SimpleGraph.Walk G u v)
:
@[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 : SimpleGraph.Walk G u v)
:
@[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 : SimpleGraph.Walk G u v)
:
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 : SimpleGraph.Walk G u v}
(hinj : Function.Injective ⇑f)
(hp : SimpleGraph.Walk.IsPath p)
:
theorem
SimpleGraph.Walk.IsPath.of_map
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
{f : G →g G'}
(hp : SimpleGraph.Walk.IsPath (SimpleGraph.Walk.map f p))
:
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 : SimpleGraph.Walk G 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 : V}
{p : SimpleGraph.Walk G 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 : V}
{p : SimpleGraph.Walk G 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 : SimpleGraph.Walk G u u}
(hinj : Function.Injective ⇑f)
:
theorem
SimpleGraph.Walk.map_isCycle_of_injective
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
{f : G →g G'}
{u : V}
{p : SimpleGraph.Walk G u u}
(hinj : Function.Injective ⇑f)
:
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]
def
SimpleGraph.Walk.mapLe
{V : Type u}
{G : SimpleGraph V}
{G' : SimpleGraph V}
(h : G ≤ G')
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Walk G' 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 : SimpleGraph.Walk G u v}
:
theorem
SimpleGraph.Walk.IsTrail.mapLe
{V : Type u}
{G : SimpleGraph V}
{G' : SimpleGraph V}
(h : G ≤ G')
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
:
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 : SimpleGraph.Walk G u v}
:
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 : SimpleGraph.Walk G u v}
:
theorem
SimpleGraph.Walk.IsPath.mapLe
{V : Type u}
{G : SimpleGraph V}
{G' : SimpleGraph V}
(h : G ≤ G')
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
:
Alias of the reverse direction of SimpleGraph.Walk.mapLe_isPath.
theorem
SimpleGraph.Walk.IsPath.of_mapLe
{V : Type u}
{G : SimpleGraph V}
{G' : SimpleGraph V}
(h : G ≤ G')
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
:
Alias of the forward 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 : SimpleGraph.Walk G u u}
:
theorem
SimpleGraph.Walk.IsCycle.of_mapLe
{V : Type u}
{G : SimpleGraph V}
{G' : SimpleGraph V}
(h : G ≤ G')
{u : V}
{p : SimpleGraph.Walk G u u}
:
Alias of the forward direction of SimpleGraph.Walk.mapLe_isCycle.
theorem
SimpleGraph.Walk.IsCycle.mapLe
{V : Type u}
{G : SimpleGraph V}
{G' : SimpleGraph V}
(h : G ≤ G')
{u : V}
{p : SimpleGraph.Walk G u u}
:
Alias of the reverse 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 : SimpleGraph.Path G u v)
:
↑(SimpleGraph.Path.map f hinj p) = SimpleGraph.Walk.map f ↑p
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 : SimpleGraph.Path G u v)
:
SimpleGraph.Path G' (f u) (f v)
Given an injective graph homomorphism, map paths to paths.
Equations
- SimpleGraph.Path.map f hinj p = { val := SimpleGraph.Walk.map f ↑p, property := (_ : SimpleGraph.Walk.IsPath (SimpleGraph.Walk.map f ↑p)) }
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)
:
Function.Injective (SimpleGraph.Path.map f hinj)
@[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 : SimpleGraph.Path G 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 : SimpleGraph.Path G u v)
:
SimpleGraph.Path G' (f u) (f v)
Given a graph embedding, map paths to paths.
Equations
Instances For
theorem
SimpleGraph.Path.mapEmbedding_injective
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
(f : G ↪g G')
(u : V)
(v : V)
:
### Transferring between graphs
def
SimpleGraph.Walk.transfer
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
(H : SimpleGraph V)
(h : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet H)
:
SimpleGraph.Walk H u v
The walk p transferred to lie in H, given that H contains its edges.
Equations
- One or more equations did not get rendered due to their size.
- SimpleGraph.Walk.transfer SimpleGraph.Walk.nil H h_2 = SimpleGraph.Walk.nil
Instances For
theorem
SimpleGraph.Walk.transfer_self
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Walk.transfer p G (_ : ∀ ⦃e : Sym2 V⦄, e ∈ SimpleGraph.Walk.edges p → e ∈ SimpleGraph.edgeSet G) = p
theorem
SimpleGraph.Walk.transfer_eq_map_of_le
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{H : SimpleGraph V}
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet H)
(GH : G ≤ H)
:
@[simp]
theorem
SimpleGraph.Walk.edges_transfer
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{H : SimpleGraph V}
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet H)
:
@[simp]
theorem
SimpleGraph.Walk.support_transfer
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{H : SimpleGraph V}
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet H)
:
@[simp]
theorem
SimpleGraph.Walk.length_transfer
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{H : SimpleGraph V}
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet H)
:
theorem
SimpleGraph.Walk.IsPath.transfer
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{p : SimpleGraph.Walk G u v}
{H : SimpleGraph V}
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet H)
(pp : SimpleGraph.Walk.IsPath p)
:
theorem
SimpleGraph.Walk.IsCycle.transfer
{V : Type u}
{G : SimpleGraph V}
{u : V}
{H : SimpleGraph V}
{q : SimpleGraph.Walk G u u}
(qc : SimpleGraph.Walk.IsCycle q)
(hq : ∀ e ∈ SimpleGraph.Walk.edges q, e ∈ SimpleGraph.edgeSet H)
:
@[simp]
theorem
SimpleGraph.Walk.transfer_transfer
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{H : SimpleGraph V}
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet H)
{K : SimpleGraph V}
(hp' : ∀ e ∈ SimpleGraph.Walk.edges (SimpleGraph.Walk.transfer p H hp), e ∈ SimpleGraph.edgeSet K)
:
SimpleGraph.Walk.transfer (SimpleGraph.Walk.transfer p H hp) K hp' = SimpleGraph.Walk.transfer p K (_ : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet K)
@[simp]
theorem
SimpleGraph.Walk.transfer_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{w : V}
{H : SimpleGraph V}
(q : SimpleGraph.Walk G v w)
(hpq : ∀ e ∈ SimpleGraph.Walk.edges (SimpleGraph.Walk.append p q), e ∈ SimpleGraph.edgeSet H)
:
SimpleGraph.Walk.transfer (SimpleGraph.Walk.append p q) H hpq = SimpleGraph.Walk.append
(SimpleGraph.Walk.transfer p H (_ : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet H))
(SimpleGraph.Walk.transfer q H (_ : ∀ e ∈ SimpleGraph.Walk.edges q, e ∈ SimpleGraph.edgeSet H))
@[simp]
theorem
SimpleGraph.Walk.reverse_transfer
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{H : SimpleGraph V}
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet H)
:
SimpleGraph.Walk.reverse (SimpleGraph.Walk.transfer p H hp) = SimpleGraph.Walk.transfer (SimpleGraph.Walk.reverse p) H
(_ : ∀ e ∈ SimpleGraph.Walk.edges (SimpleGraph.Walk.reverse p), e ∈ SimpleGraph.edgeSet H)
Deleting edges #
@[reducible]
def
SimpleGraph.Walk.toDeleteEdges
{V : Type u}
{G : SimpleGraph V}
(s : Set (Sym2 V))
{v : V}
{w : V}
(p : SimpleGraph.Walk G v w)
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∉ s)
:
SimpleGraph.Walk (SimpleGraph.deleteEdges G s) v w
Given a walk that avoids a set of edges, produce a walk in the graph with those edges deleted.
Equations
- SimpleGraph.Walk.toDeleteEdges s p hp = SimpleGraph.Walk.transfer p (SimpleGraph.deleteEdges G s) (_ : ∀ e ∈ SimpleGraph.Walk.edges p, e ∈ SimpleGraph.edgeSet (SimpleGraph.deleteEdges G s))
Instances For
@[simp]
theorem
SimpleGraph.Walk.toDeleteEdges_nil
{V : Type u}
{G : SimpleGraph V}
(s : Set (Sym2 V))
{v : V}
(hp : ∀ e ∈ SimpleGraph.Walk.edges SimpleGraph.Walk.nil, e ∉ s)
:
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 : SimpleGraph.Walk G v w)
(hp : ∀ e ∈ SimpleGraph.Walk.edges (SimpleGraph.Walk.cons h p), e ∉ s)
:
SimpleGraph.Walk.toDeleteEdges s (SimpleGraph.Walk.cons h p) hp = SimpleGraph.Walk.cons (_ : (SimpleGraph.deleteEdges G s).Adj u v)
(SimpleGraph.Walk.toDeleteEdges s p (_ : ∀ x ∈ SimpleGraph.Walk.edges p, x ∉ s))
@[inline, reducible]
abbrev
SimpleGraph.Walk.toDeleteEdge
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
(e : Sym2 V)
(p : SimpleGraph.Walk G v w)
(hp : e ∉ SimpleGraph.Walk.edges p)
:
SimpleGraph.Walk (SimpleGraph.deleteEdges G {e}) 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
- SimpleGraph.Walk.toDeleteEdge e p hp = SimpleGraph.Walk.toDeleteEdges {e} p (_ : ∀ e' ∈ SimpleGraph.Walk.edges p, e' ∉ {e})
Instances For
@[simp]
theorem
SimpleGraph.Walk.map_toDeleteEdges_eq
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
(s : Set (Sym2 V))
{p : SimpleGraph.Walk G v w}
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∉ s)
:
SimpleGraph.Walk.map (SimpleGraph.Hom.mapSpanningSubgraphs (_ : SimpleGraph.deleteEdges G s ≤ G))
(SimpleGraph.Walk.toDeleteEdges s p hp) = p
theorem
SimpleGraph.Walk.IsPath.toDeleteEdges
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
(s : Set (Sym2 V))
{p : SimpleGraph.Walk G v w}
(h : SimpleGraph.Walk.IsPath p)
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∉ s)
:
theorem
SimpleGraph.Walk.IsCycle.toDeleteEdges
{V : Type u}
{G : SimpleGraph V}
{v : V}
(s : Set (Sym2 V))
{p : SimpleGraph.Walk G v v}
(h : SimpleGraph.Walk.IsCycle p)
(hp : ∀ e ∈ SimpleGraph.Walk.edges p, e ∉ s)
:
@[simp]
theorem
SimpleGraph.Walk.toDeleteEdges_copy
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{u' : V}
{v' : V}
(s : Set (Sym2 V))
(p : SimpleGraph.Walk G u v)
(hu : u = u')
(hv : v = v')
(h : ∀ e ∈ SimpleGraph.Walk.edges (SimpleGraph.Walk.copy p hu hv), e ∉ s)
:
SimpleGraph.Walk.toDeleteEdges s (SimpleGraph.Walk.copy p hu hv) h = SimpleGraph.Walk.copy (SimpleGraph.Walk.toDeleteEdges s p (_ : ∀ e ∈ SimpleGraph.Walk.edges p, e ∉ s)) hu hv
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
- SimpleGraph.Reachable G u v = Nonempty (SimpleGraph.Walk G u v)
Instances For
theorem
SimpleGraph.reachable_iff_nonempty_univ
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
SimpleGraph.Reachable G u v ↔ Set.Nonempty Set.univ
theorem
SimpleGraph.Reachable.elim
{V : Type u}
{G : SimpleGraph V}
{p : Prop}
{u : V}
{v : V}
(h : SimpleGraph.Reachable G u v)
(hp : SimpleGraph.Walk G u v → p)
:
p
theorem
SimpleGraph.Reachable.elim_path
{V : Type u}
{G : SimpleGraph V}
{p : Prop}
{u : V}
{v : V}
(h : SimpleGraph.Reachable G u v)
(hp : SimpleGraph.Path G u v → p)
:
p
theorem
SimpleGraph.Walk.reachable
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Reachable G u v
theorem
SimpleGraph.Adj.reachable
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(h : G.Adj u v)
:
SimpleGraph.Reachable G u v
theorem
SimpleGraph.Reachable.refl
{V : Type u}
{G : SimpleGraph V}
(u : V)
:
SimpleGraph.Reachable G u u
theorem
SimpleGraph.Reachable.rfl
{V : Type u}
{G : SimpleGraph V}
{u : V}
:
SimpleGraph.Reachable G u u
theorem
SimpleGraph.Reachable.symm
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(huv : SimpleGraph.Reachable G u v)
:
SimpleGraph.Reachable G v u
theorem
SimpleGraph.reachable_comm
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
SimpleGraph.Reachable G u v ↔ SimpleGraph.Reachable G v u
theorem
SimpleGraph.Reachable.trans
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(huv : SimpleGraph.Reachable G u v)
(hvw : SimpleGraph.Reachable G v w)
:
SimpleGraph.Reachable G u w
theorem
SimpleGraph.reachable_iff_reflTransGen
{V : Type u}
{G : SimpleGraph V}
(u : V)
(v : V)
:
SimpleGraph.Reachable G 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 : SimpleGraph.Reachable G u v)
:
SimpleGraph.Reachable G' (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 : SimpleGraph.Reachable G u v)
:
SimpleGraph.Reachable G' 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}
:
SimpleGraph.Reachable G' (φ u) (φ v) ↔ SimpleGraph.Reachable G 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'}
:
SimpleGraph.Reachable G ((SimpleGraph.Iso.symm φ) v) u ↔ SimpleGraph.Reachable G' v (φ u)
The equivalence relation on vertices given by SimpleGraph.Reachable.
Equations
- SimpleGraph.reachableSetoid G = { r := SimpleGraph.Reachable G, iseqv := (_ : Equivalence (SimpleGraph.Reachable G)) }
Instances For
A graph is preconnected if every pair of vertices is reachable from one another.
Equations
- SimpleGraph.Preconnected G = ∀ (u v : V), SimpleGraph.Reachable G 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 : SimpleGraph.Preconnected G)
:
theorem
SimpleGraph.Preconnected.mono
{V : Type u}
{G : SimpleGraph V}
{G' : SimpleGraph V}
(h : G ≤ G')
(hG : SimpleGraph.Preconnected G)
:
theorem
SimpleGraph.Iso.preconnected_iff
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{H : SimpleGraph V'}
(e : G ≃g H)
:
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 : SimpleGraph.Preconnected G
- nonempty : Nonempty V
Instances For
theorem
SimpleGraph.connected_iff_exists_forall_reachable
{V : Type u}
(G : SimpleGraph V)
:
SimpleGraph.Connected G ↔ ∃ (v : V), ∀ (w : V), SimpleGraph.Reachable G v w
instance
SimpleGraph.instCoeFunConnectedForAllReachable
{V : Type u}
(G : SimpleGraph V)
:
CoeFun (SimpleGraph.Connected G) fun (x : SimpleGraph.Connected G) => ∀ (u v : V), SimpleGraph.Reachable G u v
Equations
- SimpleGraph.instCoeFunConnectedForAllReachable G = { coe := (_ : SimpleGraph.Connected G → SimpleGraph.Preconnected G) }
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 : SimpleGraph.Connected G)
:
theorem
SimpleGraph.Connected.mono
{V : Type u}
{G : SimpleGraph V}
{G' : SimpleGraph V}
(h : G ≤ G')
(hG : SimpleGraph.Connected G)
:
theorem
SimpleGraph.Iso.connected_iff
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{H : SimpleGraph V'}
(e : G ≃g H)
:
The quotient of V by the SimpleGraph.Reachable relation gives the connected
components of a graph.
Equations
Instances For
Gives the connected component containing a particular vertex.
Equations
Instances For
@[simp]
theorem
SimpleGraph.ConnectedComponent.inhabited_default
{V : Type u}
{G : SimpleGraph V}
[Inhabited V]
:
default = SimpleGraph.connectedComponentMk G default
Equations
- SimpleGraph.ConnectedComponent.inhabited = { default := SimpleGraph.connectedComponentMk G default }
theorem
SimpleGraph.ConnectedComponent.ind
{V : Type u}
{G : SimpleGraph V}
{β : SimpleGraph.ConnectedComponent G → Prop}
(h : ∀ (v : V), β (SimpleGraph.connectedComponentMk G v))
(c : SimpleGraph.ConnectedComponent G)
:
β c
theorem
SimpleGraph.ConnectedComponent.ind₂
{V : Type u}
{G : SimpleGraph V}
{β : SimpleGraph.ConnectedComponent G → SimpleGraph.ConnectedComponent G → Prop}
(h : ∀ (v w : V), β (SimpleGraph.connectedComponentMk G v) (SimpleGraph.connectedComponentMk G w))
(c : SimpleGraph.ConnectedComponent G)
(d : SimpleGraph.ConnectedComponent G)
:
β c d
@[simp]
theorem
SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
(a : G.Adj v w)
:
def
SimpleGraph.ConnectedComponent.lift
{V : Type u}
{G : SimpleGraph V}
{β : Sort u_1}
(f : V → β)
(h : ∀ (v w : V) (p : SimpleGraph.Walk G v w), SimpleGraph.Walk.IsPath p → f v = f w)
:
The ConnectedComponent specialization of Quot.lift. Provides the stronger
assumption that the vertices are connected by a path.
Equations
- SimpleGraph.ConnectedComponent.lift f h = Quot.lift f (_ : ∀ (v w : V), SimpleGraph.Reachable G v w → f v = f w)
Instances For
@[simp]
theorem
SimpleGraph.ConnectedComponent.lift_mk
{V : Type u}
{G : SimpleGraph V}
{β : Sort u_1}
{f : V → β}
{h : ∀ (v w : V) (p : SimpleGraph.Walk G v w), SimpleGraph.Walk.IsPath p → f v = f w}
{v : V}
:
theorem
SimpleGraph.ConnectedComponent.exists
{V : Type u}
{G : SimpleGraph V}
{p : SimpleGraph.ConnectedComponent G → Prop}
:
(∃ (c : SimpleGraph.ConnectedComponent G), p c) ↔ ∃ (v : V), p (SimpleGraph.connectedComponentMk G v)
theorem
SimpleGraph.ConnectedComponent.forall
{V : Type u}
{G : SimpleGraph V}
{p : SimpleGraph.ConnectedComponent G → Prop}
:
(∀ (c : SimpleGraph.ConnectedComponent G), p c) ↔ ∀ (v : V), p (SimpleGraph.connectedComponentMk G v)
theorem
SimpleGraph.Preconnected.subsingleton_connectedComponent
{V : Type u}
{G : SimpleGraph V}
(h : SimpleGraph.Preconnected G)
:
def
SimpleGraph.ConnectedComponent.map
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
(φ : G →g G')
(C : SimpleGraph.ConnectedComponent G)
:
The map on connected components induced by a graph homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SimpleGraph.ConnectedComponent.map_mk
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
(φ : G →g G')
(v : V)
:
@[simp]
theorem
SimpleGraph.ConnectedComponent.map_id
{V : Type u}
{G : SimpleGraph V}
(C : SimpleGraph.ConnectedComponent G)
:
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 : SimpleGraph.ConnectedComponent G)
(φ : 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 : SimpleGraph.ConnectedComponent G}
:
@[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 : SimpleGraph.ConnectedComponent G}
:
@[simp]
theorem
SimpleGraph.Iso.connectedComponentEquiv_apply
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
(φ : G ≃g G')
(C : SimpleGraph.ConnectedComponent G)
:
@[simp]
theorem
SimpleGraph.Iso.connectedComponentEquiv_symm_apply
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
(φ : G ≃g G')
(C : SimpleGraph.ConnectedComponent G')
:
def
SimpleGraph.Iso.connectedComponentEquiv
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
(φ : G ≃g G')
:
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.connectedComponentEquiv SimpleGraph.Iso.refl = Equiv.refl (SimpleGraph.ConnectedComponent G)
@[simp]
theorem
SimpleGraph.Iso.connectedComponentEquiv_symm
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
(φ : G ≃g G')
:
@[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'')
:
def
SimpleGraph.ConnectedComponent.supp
{V : Type u}
{G : SimpleGraph V}
(C : SimpleGraph.ConnectedComponent G)
:
Set V
The set of vertices in a connected component of a graph.
Equations
- SimpleGraph.ConnectedComponent.supp C = {v : V | SimpleGraph.connectedComponentMk G 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 : SimpleGraph.ConnectedComponent G}
{D : SimpleGraph.ConnectedComponent G}
:
instance
SimpleGraph.ConnectedComponent.instSetLikeConnectedComponent
{V : Type u}
{G : SimpleGraph V}
:
Equations
- SimpleGraph.ConnectedComponent.instSetLikeConnectedComponent = { coe := SimpleGraph.ConnectedComponent.supp, coe_injective' := (_ : Function.Injective SimpleGraph.ConnectedComponent.supp) }
@[simp]
theorem
SimpleGraph.ConnectedComponent.mem_supp_iff
{V : Type u}
{G : SimpleGraph V}
(C : SimpleGraph.ConnectedComponent G)
(v : V)
:
theorem
SimpleGraph.ConnectedComponent.connectedComponentMk_mem
{V : Type u}
{G : SimpleGraph V}
{v : V}
:
def
SimpleGraph.ConnectedComponent.isoEquivSupp
{V : Type u}
{V' : Type v}
{G : SimpleGraph V}
{G' : SimpleGraph V'}
(φ : G ≃g G')
(C : SimpleGraph.ConnectedComponent G)
:
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 : SimpleGraph.Preconnected G)
(u : V)
(v : V)
:
Set.Nonempty Set.univ
theorem
SimpleGraph.Connected.set_univ_walk_nonempty
{V : Type u}
{G : SimpleGraph V}
(hconn : SimpleGraph.Connected G)
(u : V)
(v : V)
:
Set.Nonempty Set.univ
Walks as subgraphs #
def
SimpleGraph.Walk.toSubgraph
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
SimpleGraph.Walk G u v → SimpleGraph.Subgraph G
The subgraph consisting of the vertices and edges of the walk.
Equations
- SimpleGraph.Walk.toSubgraph SimpleGraph.Walk.nil = SimpleGraph.singletonSubgraph G u
- SimpleGraph.Walk.toSubgraph (SimpleGraph.Walk.cons h q) = SimpleGraph.subgraphOfAdj G h ⊔ SimpleGraph.Walk.toSubgraph q
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.toSubgraph (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil) = SimpleGraph.subgraphOfAdj G h
theorem
SimpleGraph.Walk.mem_verts_toSubgraph
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
:
w ∈ (SimpleGraph.Walk.toSubgraph p).verts ↔ w ∈ SimpleGraph.Walk.support p
theorem
SimpleGraph.Walk.start_mem_verts_toSubgraph
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
u ∈ (SimpleGraph.Walk.toSubgraph p).verts
theorem
SimpleGraph.Walk.end_mem_verts_toSubgraph
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
v ∈ (SimpleGraph.Walk.toSubgraph p).verts
@[simp]
theorem
SimpleGraph.Walk.verts_toSubgraph
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
(SimpleGraph.Walk.toSubgraph p).verts = {w : V | w ∈ SimpleGraph.Walk.support p}
theorem
SimpleGraph.Walk.mem_edges_toSubgraph
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
{e : Sym2 V}
:
@[simp]
theorem
SimpleGraph.Walk.edgeSet_toSubgraph
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Subgraph.edgeSet (SimpleGraph.Walk.toSubgraph p) = {e : Sym2 V | e ∈ SimpleGraph.Walk.edges p}
@[simp]
theorem
SimpleGraph.Walk.toSubgraph_append
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
(q : SimpleGraph.Walk G v w)
:
@[simp]
theorem
SimpleGraph.Walk.toSubgraph_reverse
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.toSubgraph_rotate
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
[DecidableEq V]
(c : SimpleGraph.Walk G v v)
(h : u ∈ SimpleGraph.Walk.support c)
:
@[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 : SimpleGraph.Walk G u v)
:
@[simp]
theorem
SimpleGraph.Walk.finite_neighborSet_toSubgraph
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{w : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Walk.toSubgraph_le_induce_support
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Walk.toSubgraph p ≤ SimpleGraph.Subgraph.induce ⊤ {v_1 : V | v_1 ∈ SimpleGraph.Walk.support p}
Walks of a given length #
theorem
SimpleGraph.set_walk_self_length_zero_eq
{V : Type u}
{G : SimpleGraph V}
(u : V)
:
{p : SimpleGraph.Walk G u u | SimpleGraph.Walk.length p = 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 : SimpleGraph.Walk G u v | SimpleGraph.Walk.length p = 0} = ∅
theorem
SimpleGraph.set_walk_length_succ_eq
{V : Type u}
{G : SimpleGraph V}
(u : V)
(v : V)
(n : ℕ)
:
{p : SimpleGraph.Walk G u v | SimpleGraph.Walk.length p = Nat.succ n} = ⋃ (w : V),
⋃ (h : G.Adj u w), SimpleGraph.Walk.cons h '' {p' : SimpleGraph.Walk G w v | SimpleGraph.Walk.length p' = n}
@[simp]
theorem
SimpleGraph.walkLengthTwoEquivCommonNeighbors_apply_coe
{V : Type u}
(G : SimpleGraph V)
(u : V)
(v : V)
(p : { p : SimpleGraph.Walk G u v // SimpleGraph.Walk.length p = 2 })
:
↑((SimpleGraph.walkLengthTwoEquivCommonNeighbors G u v) p) = SimpleGraph.Walk.getVert (↑p) 1
@[simp]
theorem
SimpleGraph.walkLengthTwoEquivCommonNeighbors_symm_apply_coe
{V : Type u}
(G : SimpleGraph V)
(u : V)
(v : V)
(w : ↑(SimpleGraph.commonNeighbors G u v))
:
↑((SimpleGraph.walkLengthTwoEquivCommonNeighbors G u v).symm w) = SimpleGraph.Walk.concat (SimpleGraph.Adj.toWalk (_ : ↑w ∈ SimpleGraph.neighborSet G u)) (_ : G.Adj (↑w) v)
def
SimpleGraph.walkLengthTwoEquivCommonNeighbors
{V : Type u}
(G : SimpleGraph V)
(u : V)
(v : V)
:
{ p : SimpleGraph.Walk G u v // SimpleGraph.Walk.length p = 2 } ≃ ↑(SimpleGraph.commonNeighbors G 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]
[SimpleGraph.LocallyFinite G]
(n : ℕ)
(u : V)
(v : V)
:
Finset (SimpleGraph.Walk G 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.
- SimpleGraph.finsetWalkLength G 0 u v = if h : u = v then (_ : v = u) ▸ {SimpleGraph.Walk.nil} else ∅
Instances For
theorem
SimpleGraph.coe_finsetWalkLength_eq
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[SimpleGraph.LocallyFinite G]
(n : ℕ)
(u : V)
(v : V)
:
↑(SimpleGraph.finsetWalkLength G n u v) = {p : SimpleGraph.Walk G u v | SimpleGraph.Walk.length p = n}
theorem
SimpleGraph.Walk.mem_finsetWalkLength_iff_length_eq
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
[SimpleGraph.LocallyFinite G]
{n : ℕ}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
p ∈ SimpleGraph.finsetWalkLength G n u v ↔ SimpleGraph.Walk.length p = n
instance
SimpleGraph.fintypeSetWalkLength
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[SimpleGraph.LocallyFinite G]
(u : V)
(v : V)
(n : ℕ)
:
Fintype ↑{p : SimpleGraph.Walk G u v | SimpleGraph.Walk.length p = n}
Equations
- One or more equations did not get rendered due to their size.
instance
SimpleGraph.fintypeSubtypeWalkLength
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[SimpleGraph.LocallyFinite G]
(u : V)
(v : V)
(n : ℕ)
:
Fintype { p : SimpleGraph.Walk G u v // SimpleGraph.Walk.length p = n }
Equations
- SimpleGraph.fintypeSubtypeWalkLength G u v n = SimpleGraph.fintypeSetWalkLength G u v n
theorem
SimpleGraph.set_walk_length_toFinset_eq
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[SimpleGraph.LocallyFinite G]
(n : ℕ)
(u : V)
(v : V)
:
Set.toFinset {p : SimpleGraph.Walk G u v | SimpleGraph.Walk.length p = n} = SimpleGraph.finsetWalkLength G n u v
theorem
SimpleGraph.card_set_walk_length_eq
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[SimpleGraph.LocallyFinite G]
(u : V)
(v : V)
(n : ℕ)
:
Fintype.card ↑{p : SimpleGraph.Walk G u v | SimpleGraph.Walk.length p = n} = (SimpleGraph.finsetWalkLength G n u v).card
instance
SimpleGraph.fintypeSetPathLength
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[SimpleGraph.LocallyFinite G]
(u : V)
(v : V)
(n : ℕ)
:
Fintype ↑{p : SimpleGraph.Walk G u v | SimpleGraph.Walk.IsPath p ∧ SimpleGraph.Walk.length p = n}
Equations
- One or more equations did not get rendered due to their size.
theorem
SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[Fintype V]
[DecidableRel G.Adj]
(u : V)
(v : V)
:
SimpleGraph.Reachable G u v ↔ ∃ (n : Fin (Fintype.card V)), (SimpleGraph.finsetWalkLength G (↑n) u v).Nonempty
instance
SimpleGraph.instDecidableRelReachable
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[Fintype V]
[DecidableRel G.Adj]
:
Equations
- One or more equations did not get rendered due to their size.
instance
SimpleGraph.instFintypeConnectedComponent
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[Fintype V]
[DecidableRel G.Adj]
:
instance
SimpleGraph.instDecidablePreconnected
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[Fintype V]
[DecidableRel G.Adj]
:
Equations
- SimpleGraph.instDecidablePreconnected G = inferInstanceAs (Decidable (∀ (u v : V), SimpleGraph.Reachable G u v))
instance
SimpleGraph.instDecidableConnected
{V : Type u}
(G : SimpleGraph V)
[DecidableEq V]
[Fintype V]
[DecidableRel G.Adj]
:
Equations
- One or more equations did not get rendered due to their size.
Bridge edges #
An edge of a graph is a bridge if, after removing it, its incident vertices are no longer reachable from one another.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
SimpleGraph.isBridge_iff
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
:
SimpleGraph.IsBridge G s(u, v) ↔ G.Adj u v ∧ ¬SimpleGraph.Reachable (G \ SimpleGraph.fromEdgeSet {s(u, v)}) u v
theorem
SimpleGraph.reachable_delete_edges_iff_exists_walk
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
:
SimpleGraph.Reachable (G \ SimpleGraph.fromEdgeSet {s(v, w)}) v w ↔ ∃ (p : SimpleGraph.Walk G v w), s(v, w) ∉ SimpleGraph.Walk.edges p
theorem
SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
:
SimpleGraph.IsBridge G s(v, w) ↔ G.Adj v w ∧ ∀ (p : SimpleGraph.Walk G v w), s(v, w) ∈ SimpleGraph.Walk.edges p
theorem
SimpleGraph.reachable_deleteEdges_iff_exists_cycle.aux
{V : Type u}
{G : SimpleGraph V}
[DecidableEq V]
{u : V}
{v : V}
{w : V}
(hb : ∀ (p : SimpleGraph.Walk G v w), s(v, w) ∈ SimpleGraph.Walk.edges p)
(c : SimpleGraph.Walk G u u)
(hc : SimpleGraph.Walk.IsTrail c)
(he : s(v, w) ∈ SimpleGraph.Walk.edges c)
(hw : w ∈ SimpleGraph.Walk.support (SimpleGraph.Walk.takeUntil c v (_ : v ∈ SimpleGraph.Walk.support c)))
:
theorem
SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
:
G.Adj v w ∧ SimpleGraph.Reachable (G \ SimpleGraph.fromEdgeSet {s(v, w)}) v w ↔ ∃ (u : V) (p : SimpleGraph.Walk G u u), SimpleGraph.Walk.IsCycle p ∧ s(v, w) ∈ SimpleGraph.Walk.edges p
theorem
SimpleGraph.isBridge_iff_adj_and_forall_cycle_not_mem
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
:
SimpleGraph.IsBridge G s(v, w) ↔ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : SimpleGraph.Walk G u u), SimpleGraph.Walk.IsCycle p → s(v, w) ∉ SimpleGraph.Walk.edges p
theorem
SimpleGraph.isBridge_iff_mem_and_forall_cycle_not_mem
{V : Type u}
{G : SimpleGraph V}
{e : Sym2 V}
:
SimpleGraph.IsBridge G e ↔ e ∈ SimpleGraph.edgeSet G ∧ ∀ ⦃u : V⦄ (p : SimpleGraph.Walk G u u), SimpleGraph.Walk.IsCycle p → e ∉ SimpleGraph.Walk.edges p