inductive Graph.IsWalk {α : Type u_1} {β : Type u_2} (G : Graph α β) : WList α β → Prop

G.IsWalk w means that w : WList α β is a walk of G : Graph α β.

• nil {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : G.IsWalk (WList.nil x)
• cons {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {e : β} {w : WList α β} (hw : G.IsWalk w) (h : G.IsLink e x w.first) : G.IsWalk (WList.cons x e w)

@[simp]

theorem Graph.nil_isWalk_iff {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} : G.IsWalk (WList.nil x) ↔ x ∈ G.vertexSet

@[simp]

theorem Graph.cons_isWalk_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {w : WList α β} : G.IsWalk (WList.cons x e w) ↔ G.IsLink e x w.first ∧ G.IsWalk w

@[simp]

theorem Graph.IsWalk.of_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {w : WList α β} (hw : G.IsWalk (WList.cons x e w)) : G.IsWalk w

theorem Graph.IsWalk.vertex_mem_of_mem {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) (hmem : x ∈ w) : x ∈ G.vertexSet

theorem Graph.IsWalk.edge_mem_of_mem {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) (hmem : e ∈ w.edge) : e ∈ G.edgeSet

theorem Graph.IsWalk.vertex_mem_of_edge_mem {α : Type u_1} {β : Type u_2} {u : α} {e : β} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) (he : e ∈ w.edge) (heu : G.Inc e u) : u ∈ w

theorem Graph.IsWalk.first_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) : w.first ∈ G.vertexSet

theorem Graph.IsWalk.last_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) : w.last ∈ G.vertexSet

theorem Graph.IsWalk.vertexSet_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (hVd : G.IsWalk w) : w.vertexSet ⊆ G.vertexSet

theorem Graph.IsWalk.edgeSet_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) : w.edgeSet ⊆ G.edgeSet

@[simp]

theorem Graph.not_isWalk_bot {α : Type u_1} {β : Type u_2} {w : WList α β} : ¬⊥.IsWalk w

theorem Graph.IsWalk.mem_of_mem_edge_of_inc {α : Type u_1} {β : Type u_2} {u : α} {e : β} {G : Graph α β} {w : WList α β} (hw : G.IsWalk w) (he : e ∈ w.edge) (h : G.Inc e u) : u ∈ w

theorem Graph.IsWalk.sublist {α : Type u_1} {β : Type u_2} {G : Graph α β} {w₁ w₂ : WList α β} (hw₂ : G.IsWalk w₂) (h : w₁.IsSublist w₂) : G.IsWalk w₁

theorem Graph.IsWalk.prefix {α : Type u_1} {β : Type u_2} {G : Graph α β} {w w₁ : WList α β} (hw : G.IsWalk w) (h : w₁.IsPrefix w) : G.IsWalk w₁

theorem Graph.IsWalk.suffix {α : Type u_1} {β : Type u_2} {G : Graph α β} {w w₁ : WList α β} (hw : G.IsWalk w) (h : w₁.IsSuffix w) : G.IsWalk w₁

theorem Graph.IsWalk.tail {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (hw : G.IsWalk w) : G.IsWalk w.tail

theorem Graph.IsWalk.dropLast {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (hw : G.IsWalk w) : G.IsWalk w.dropLast

theorem Graph.IsWalk.append {α : Type u_1} {β : Type u_2} {G : Graph α β} {w₁ w₂ : WList α β} (h₁ : G.IsWalk w₁) (h₂ : G.IsWalk w₂) (h : w₁.last = w₂.first) : G.IsWalk (w₁ ++ w₂)

theorem Graph.IsWalk.concat {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) (he : G.IsLink e w.last x) : G.IsWalk (w.concat e x)

theorem Graph.IsWalk.of_concat {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {w : WList α β} (h : G.IsWalk (w.concat e x)) : G.IsWalk w

@[simp]

theorem Graph.concat_isWalk_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {w : WList α β} : G.IsWalk (w.concat e x) ↔ G.IsWalk w ∧ G.IsLink e w.last x

theorem Graph.IsWalk.of_append_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {w₁ w₂ : WList α β} (h : G.IsWalk (w₁ ++ w₂)) (h_eq : w₁.last = w₂.first) : G.IsWalk w₁

theorem Graph.IsWalk.of_append_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {w₁ w₂ : WList α β} (h : G.IsWalk (w₁ ++ w₂)) : G.IsWalk w₂

theorem Graph.IsWalk.last_eq_first {α : Type u_1} {β : Type u_2} {G : Graph α β} {w₁ w₂ : WList α β} (h : G.IsWalk (w₁ ++ w₂)) (hw₁ : G.IsWalk w₁) (hne : w₁.Nonempty) : w₁.last = w₂.first

theorem Graph.IsWalk.reverse {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (hw : G.IsWalk w) : G.IsWalk w.reverse

@[simp]

theorem Graph.isWalk_reverse_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} : G.IsWalk w.reverse ↔ G.IsWalk w

theorem Graph.IsWalk.deloop {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} [DecidableEq α] (h : G.IsWalk w) : G.IsWalk w.deloop

theorem Graph.IsWalk.deloop_edge_eq_filter {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} [DecidableEq α] [DecidablePred fun (x : β) => ∀ (x_1 : α), ¬G.IsLoopAt x x_1] (h : G.IsWalk w) : w.deloop.edge = List.filter (fun (x : β) => decide (∀ (x_1 : α), ¬G.IsLoopAt x x_1)) w.edge

@[simp]

theorem Graph.IsWalk.mem_deloop_edge_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} [DecidableEq α] (h : G.IsWalk w) (e : β) : e ∈ w.deloop.edge ↔ e ∈ w.edge ∧ ∀ (x : α), ¬G.IsLoopAt e x

theorem Graph.edgeRemove_first {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {w : WList α β} (hF : ∀ e ∈ w.edge, e ∈ F → ∃ (x : α), G.IsLoopAt e x) [DecidablePred fun (x : β) => x ∈ F] (hw : G.IsWalk w) : (WList.edgeRemove F w).first = w.first

theorem Graph.edgeRemove_isSublist {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {w : WList α β} (hF : ∀ e ∈ w.edge, e ∈ F → ∃ (x : α), G.IsLoopAt e x) [DecidablePred fun (x : β) => x ∈ F] (hw : G.IsWalk w) : (WList.edgeRemove F w).IsSublist w

@[simp]

theorem Graph.mem_edgeRemove_iff {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {F : Set β} {w : WList α β} (hF : ∀ e ∈ w.edge, e ∈ F → ∃ (x : α), G.IsLoopAt e x) [DecidablePred fun (x : β) => x ∈ F] (hw : G.IsWalk w) : x ∈ WList.edgeRemove F w ↔ x ∈ w

theorem Graph.IsWalk.edgeRemove {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {w : WList α β} [DecidablePred fun (x : β) => x ∈ F] (hw : G.IsWalk w) (hF : ∀ e ∈ w.edge, e ∈ F → ∃ (x : α), G.IsLoopAt e x) : G.IsWalk (WList.edgeRemove F w)

theorem Graph.deloop_isSublist_edgeRemove {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {w : WList α β} [DecidableEq α] [DecidablePred fun (x : β) => x ∈ F] (hw : G.IsWalk w) (hF : ∀ e ∈ w.edge, e ∈ F → ∃ (x : α), G.IsLoopAt e x) : w.deloop.IsSublist (WList.edgeRemove F w)

theorem Graph.edgeRemove_eq_deloop {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {w : WList α β} [DecidableEq α] [DecidablePred fun (x : β) => x ∈ F] (hw : G.IsWalk w) (hF : ∀ e ∈ w.edge, e ∈ F ↔ ∃ (x : α), G.IsLoopAt e x) : WList.edgeRemove F w = w.deloop

theorem Graph.edgeRemove_eq_self_of_noloop {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {w : WList α β} [DecidablePred fun (x : β) => x ∈ F] (hw : G.IsWalk w) (hF : ∀ e ∈ w.edge, e ∈ F → ∃ (x : α), G.IsLoopAt e x) (hnl : w.NoLoop) : WList.edgeRemove F w = w

theorem Graph.IsWalk.of_forall_isLink {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : G.IsWalk w) (he : ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → H.IsLink e x y) (hne : w.Nonempty) : H.IsWalk w

theorem Graph.IsWalk.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : H.IsWalk w) (hle : H ≤ G) : G.IsWalk w

theorem Graph.IsWalk.isWalk_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : G.IsWalk w) (hle : H ≤ G) (hE : w.edgeSet ⊆ H.edgeSet) (hfirst : w.first ∈ H.vertexSet) : H.IsWalk w

theorem Graph.IsWalk.isWalk_isInducedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : G.IsWalk w) (hind : H.IsInducedSubgraph G) (hX : w.vertexSet ⊆ H.vertexSet) : H.IsWalk w

theorem Graph.IsWalk.subset_of_first_mem_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : G.IsWalk w) (hcl : H.IsClosedSubgraph G) (hfirst : w.first ∈ H.vertexSet) : w.vertexSet ⊆ H.vertexSet

theorem Graph.IsWalk.subset_of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : G.IsWalk w) (hcl : H.IsClosedSubgraph G) (hx : ∃ x ∈ w.vertexSet, x ∈ H.vertexSet) : w.vertexSet ⊆ H.vertexSet

theorem Graph.IsWalk.isWalk_isClosedSubgraph_of_first_mem {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : G.IsWalk w) (hcl : H.IsClosedSubgraph G) (hfirst : w.first ∈ H.vertexSet) : H.IsWalk w

theorem Graph.IsWalk.isWalk_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : G.IsWalk w) (hcl : H.IsClosedSubgraph G) (hx : ∃ x ∈ w.vertexSet, x ∈ H.vertexSet) : H.IsWalk w

theorem Graph.IsWalk.isWalk_le_of_nonempty {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (h : G.IsWalk w) (hle : H ≤ G) (hE : w.edgeSet ⊆ H.edgeSet) (hne : w.Nonempty) : H.IsWalk w

theorem Graph.IsWalk.isLink_mono {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) (hexy : w.IsLink e x y) : G.IsLink e x y

theorem Graph.IsWalk.isLink_of_dInc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) (hexy : w.DInc e x y) : G.IsLink e x y

theorem Graph.IsWalk.wellFormed {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) : w.WellFormed

theorem Graph.IsWalk.isLink_iff_isLink_of_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) (hew : e ∈ w.edge) : w.IsLink e x y ↔ G.IsLink e x y

theorem Graph.IsWalk.eq_of_edge_eq_first_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {w₁ w₂ : WList α β} (h₁ : G.IsWalk w₁) (h₂ : G.IsWalk w₂) (h_first : w₁.first = w₂.first) (h_edge : w₁.edge = w₂.edge) : w₁ = w₂

theorem Graph.IsWalk.not_loopAt_of_noLoop {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) (hloop : w.NoLoop) (he : e ∈ w.edge) (x : α) : ¬G.IsLoopAt e x

structure Graph.IsWalkFrom {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) (w : WList α β) : Prop

G.IsWalkFrom S T w means that w is a walk of G with one end in S and the other in T.

• isWalk : G.IsWalk w
• first_mem : w.first ∈ S
• last_mem : w.last ∈ T

theorem Graph.isWalkFrom_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) (w : WList α β) : G.IsWalkFrom S T w ↔ G.IsWalk w ∧ w.first ∈ S ∧ w.last ∈ T

theorem Graph.IsWalkFrom.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} {S T : Set α} (h : G.IsWalkFrom S T w) (hle : G ≤ H) : H.IsWalkFrom S T w

theorem Graph.IsWalkFrom.reverse {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {S T : Set α} (h : G.IsWalkFrom S T w) : G.IsWalkFrom T S w.reverse

theorem Graph.IsWalk.of_mem_mem {α : Type u_1} {β : Type u_2} {u v : α} {G : Graph α β} {w : WList α β} {S T : Set α} (h : G.IsWalk w) (hu : u ∈ w.vertexSet ∩ S) (hv : v ∈ w.vertexSet ∩ T) : ∃ (W : WList α β), G.IsWalkFrom S T W ∧ (W.IsInfix w ∨ W.reverse.IsInfix w)

def Graph.IsLink.walk {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (_h : G.IsLink e u v) : WList α β

The walk corresponding to an incidence G.IsLink e u v.

Equations

• _h.walk = WList.cons u e (WList.nil v)

@[simp]

theorem Graph.IsLink.walk_nonempty {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) : h.walk.Nonempty

@[simp]

theorem Graph.IsLink.walk_first {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) : h.walk.first = u

@[simp]

theorem Graph.IsLink.walk_last {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) : h.walk.last = v

@[simp]

theorem Graph.IsLink.walk_vertex {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) : h.walk.vertex = [u, v]

@[simp]

theorem Graph.IsLink.mem_walk_iff {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) (x : α) : x ∈ h.walk ↔ x = u ∨ x = v

@[simp]

theorem Graph.IsLink.walk_vertexSet {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) : h.walk.vertexSet = {u, v}

@[simp]

theorem Graph.IsLink.walk_edge {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) : h.walk.edge = [e]

@[simp]

theorem Graph.IsLink.walk_edgeSet {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) : h.walk.edgeSet = {e}

@[simp]

theorem Graph.IsLink.walk_length {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) : h.walk.length = 1

@[simp]

theorem Graph.IsLink.walk_internalVertexSet {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) : h.walk.internalVertexSet = ∅

@[simp]

theorem Graph.IsLink.walk_isWalk {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) : G.IsWalk h.walk

theorem Graph.Isolated.eq_last_of_mem {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hisol : G.Isolated x) {w : WList α β} (hw : G.IsWalk w) (hx : x ∈ w) : x = w.last

theorem Graph.Isolated.eq_first_of_mem {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {w : WList α β} (hisol : G.Isolated x) (hw : G.IsWalk w) (hx : x ∈ w) : x = w.first

theorem Graph.Isolated.isWalk_nil_of_mem {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {w : WList α β} (hisol : G.Isolated x) (hw : G.IsWalk w) (hx : x ∈ w) : w.Nil

theorem Graph.Isolated.eq_nil_of_mem {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {w : WList α β} (hisol : G.Isolated x) (hw : G.IsWalk w) (hx : x ∈ w) : w = WList.nil x

theorem Graph.IsWalk.induce {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} (hw : G.IsWalk w) (hX : w.vertexSet ⊆ X) : G[X].IsWalk w

theorem Graph.isWalk_induce_iff' {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} (hw : w.Nonempty) : G[X].IsWalk w ↔ G.IsWalk w ∧ w.vertexSet ⊆ X

theorem Graph.isWalk_induce_iff_of_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} (hXV : X ⊆ G.vertexSet) : G[X].IsWalk w ↔ G.IsWalk w ∧ w.vertexSet ⊆ X

This is almost true without the X ⊆ V(G) assumption; the exception is where w is a nil walk on a vertex in X \ V(G).

theorem Graph.isWalk_induce_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} : G[X].IsWalk w ↔ (∃ x ∈ X \ G.vertexSet, w = WList.nil x) ∨ G.IsWalk w ∧ w.vertexSet ⊆ X

theorem Graph.IsWalk.vertexSet_subset_of_induce {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} (hw : G[X].IsWalk w) : w.vertexSet ⊆ X

@[simp]

theorem Graph.isWalk_deleteVerts_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} : (G.deleteVerts X).IsWalk w ↔ G.IsWalk w ∧ Disjoint w.vertexSet X

theorem Graph.IsWalk.deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} (hw : G.IsWalk w) (hdisj : Disjoint w.vertexSet X) : (G.deleteVerts X).IsWalk w

theorem Graph.IsWalk.disjoint_of_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} (hw : (G.deleteVerts X).IsWalk w) : Disjoint w.vertexSet X

theorem Graph.IsWalk.restrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {w : WList α β} (hw : G.IsWalk w) (hE : w.edgeSet ⊆ F) : (G.restrict F).IsWalk w

@[simp]

theorem Graph.isWalk_restrict_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {F : Set β} : (G.restrict F).IsWalk w ↔ G.IsWalk w ∧ w.edgeSet ⊆ F

theorem Graph.IsWalk.edgeSet_subset_of_restrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {w : WList α β} (hw : (G.restrict F).IsWalk w) : w.edgeSet ⊆ F

@[simp]

theorem Graph.isWalk_deleteEdges_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {F : Set β} : (G.deleteEdges F).IsWalk w ↔ G.IsWalk w ∧ Disjoint w.edgeSet F

theorem Graph.IsWalk.deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {w : WList α β} (hw : G.IsWalk w) (hdisj : Disjoint w.edgeSet F) : (G.deleteEdges F).IsWalk w

theorem Graph.IsWalk.disjoint_of_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {w : WList α β} (hw : (G.deleteEdges F).IsWalk w) : Disjoint w.edgeSet F

theorem Graph.IsWalk.isWalk_left_of_subset {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (hw : (G ∪ H).IsWalk w) (hE : w.edgeSet ⊆ G.edgeSet) (h1 : w.first ∈ G.vertexSet) : G.IsWalk w

theorem Graph.IsWalk.isWalk_left_of_subset_of_nonempty {α : Type u_1} {β : Type u_2} {G H : Graph α β} {w : WList α β} (hw : (G ∪ H).IsWalk w) (hE : w.edgeSet ⊆ G.edgeSet) (hne : w.Nonempty) : G.IsWalk w

theorem Graph.IsWalk.eq_append_cons_of_edge_mem {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {W : WList α β} (hW : G.IsWalk W) (heW : e ∈ W.edge) : ∃ (W₁ : WList α β) (W₂ : WList α β), G.IsWalk W₁ ∧ G.IsWalk W₂ ∧ e ∉ W₁.edge ∧ W = W₁ ++ WList.cons W₁.last e W₂

theorem Graph.isWalk_iff_forall_isLink_get_of_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} (hW : W.Nonempty) : G.IsWalk W ↔ ∀ (i : ℕ) (hi : i < W.length), G.IsLink W.edge[i] (W.get i) (W.get (i + 1))

theorem Graph.isWalk_zip_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (a : List α) (b : List β) (hab : b.length + 1 = a.length) : G.IsWalk (WList.zip a b hab) ↔ a[0] ∈ G.vertexSet ∧ ∀ (i : ℕ) (hi : i + 1 < a.length), G.IsLink b[i] a[i] a[i + 1]

@[simp]

theorem Graph.reverse_isWalk_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} : G.IsWalk w.reverse ↔ G.IsWalk w

theorem Graph.IsWalk.nontrivial_of_ne_not_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) (hne : w.first ≠ w.last) (hadj : ¬G.Adj w.first w.last) : w.Nontrivial

def WList.toGraph {α : Type u_1} {β : Type u_2} : WList α β → Graph α β

Turn w : WList α β into a Graph α β. If the list is not well-formed (i.e. it contains an edge appearing twice with different ends), then the last occurence of the edge determines its ends in w.toGraph.

Equations

• (WList.nil u).toGraph = Graph.noEdge {u} β
• (WList.cons u e w).toGraph = w.toGraph ∪ Graph.singleEdge u w.first e

@[simp]

theorem WList.toGraph_nil {α : Type u_1} {β : Type u_2} {u : α} : (nil u).toGraph = Graph.noEdge {u} β

@[simp]

theorem WList.toGraph_cons {α : Type u_1} {β : Type u_2} {u : α} {e : β} {w : WList α β} : (cons u e w).toGraph = w.toGraph ∪ Graph.singleEdge u w.first e

theorem WList.toGraph_concat {α : Type u_1} {β : Type u_2} (w : WList α β) (e : β) (u : α) : (w.concat e u).toGraph = Graph.singleEdge u w.last e ∪ w.toGraph

@[simp]

theorem WList.toGraph_vertexSet {α : Type u_1} {β : Type u_2} (w : WList α β) : w.toGraph.vertexSet = w.vertexSet

@[simp]

theorem WList.toGraph_edgeSet {α : Type u_1} {β : Type u_2} (w : WList α β) : w.toGraph.edgeSet = w.edgeSet

theorem WList.toGraph_vertexSet_nonempty {α : Type u_1} {β : Type u_2} (w : WList α β) : w.toGraph.vertexSet.Nonempty

@[simp]

theorem WList.WellFormed.toGraph_isLink {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.WellFormed) : w.toGraph.IsLink = w.IsLink

@[simp]

theorem WList.WellFormed.toGraph_inc {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.WellFormed) : w.toGraph.Inc = w.Inc

theorem WList.IsSublist.toGraph_le {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.IsSublist w₂) (hw₂ : w₂.WellFormed) : w₁.toGraph ≤ w₂.toGraph

theorem WList.WellFormed.reverse_toGraph {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.WellFormed) : w.reverse.toGraph = w.toGraph

theorem WList.WellFormed.isWalk_toGraph {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.WellFormed) : w.toGraph.IsWalk w

theorem WList.Nontrivial.disjoint_edgeSet_of_disjoint_internalVertexSet {α : Type u_1} {β : Type u_2} {w : WList α β} {G H : Graph α β} (hw : w.Nontrivial) (hle : H ≤ G) (hW : G.IsWalk w) (hdisj : Disjoint w.internalVertexSet H.vertexSet) : Disjoint w.edgeSet H.edgeSet

If a nontrivial walk of G has no internal vertex in V(H), then none of its edges lie in E(H). Needs Nontrivial: a one-edge walk between two vertices of H has empty internal set.

theorem Graph.IsWalk.toGraph_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) : w.toGraph ≤ G

theorem WList.WellFormed.toGraph_le_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} (hW : W.WellFormed) : W.toGraph ≤ G ↔ G.IsWalk W

theorem Graph.IsWalk.edgeSet_subset_edgeSet_induce {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (hw : G.IsWalk w) : w.edgeSet ⊆ G[w.vertexSet].edgeSet

theorem Graph.IsWalk.toGraph_eq_induce_restrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (h : G.IsWalk w) : w.toGraph = G[w.vertexSet].restrict w.edgeSet

theorem Graph.IsWalk.le_of_edgeSet_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {w₁ w₂ : WList α β} (hw₁ : G.IsWalk w₁) (hne : w₁.Nonempty) (hw₂ : G.IsWalk w₂) (hss : w₁.edgeSet ⊆ w₂.edgeSet) : w₁.toGraph ≤ w₂.toGraph