Trails

structure Graph.IsTrail {α : Type u_1} {β : Type u_2} (G : Graph α β) (W : WList α β) : Prop

G.IsTrail w means that w is a walk of G with no repeated edges.

• isWalk : G.IsWalk W
• edge_nodup : W.edge.Nodup

theorem Graph.isTrail_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (W : WList α β) : G.IsTrail W ↔ G.IsWalk W ∧ W.edge.Nodup

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

@[simp]

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

@[simp]

theorem Graph.cons_isTrail_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {w : WList α β} : G.IsTrail (WList.cons x e w) ↔ G.IsTrail w ∧ G.IsLink e x w.first ∧ e ∉ w.edge

theorem Graph.IsTrail.cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {w : WList α β} (hw : G.IsTrail w) (he : G.IsLink e x w.first) (hew : e ∉ w.edge) : G.IsTrail (WList.cons x e w)

@[simp]

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

theorem Graph.nil_isTrail {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hx : x ∈ G.vertexSet) : G.IsTrail (WList.nil x)

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

@[simp]

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

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

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

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

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

theorem Graph.isTrail_induce_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} (hXV : X ⊆ G.vertexSet) : G[X].IsTrail w ↔ G.IsTrail 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.isTrail_induce_iff' {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} (hw : w.Nonempty) : G[X].IsTrail w ↔ G.IsTrail w ∧ w.vertexSet ⊆ X

@[simp]

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

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

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

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

theorem Graph.IsTrail.dInc_iff_eq_of_dInc {α : Type u_1} {β : Type u_2} {x y u v : α} {e : β} {G : Graph α β} {W : WList α β} (hW : G.IsTrail W) (he : W.DInc e u v) : W.DInc e x y ↔ x = u ∧ y = v

theorem Graph.IsTrail.idxOf_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} [DecidableEq α] {a b : α} (hw : G.IsTrail w) (ha : a ∈ w) (hb : b ∈ w) (he : w.idxOf b = w.idxOf a + 1) : G.Adj a b

theorem Graph.IsTrail.first_eq_of_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {w : WList α β} (hT : G.IsTrail (WList.cons x e w)) (hl : G.IsLink e x y) : w.first = y

@[simp]

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

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

Paths

structure Graph.IsPath {α : Type u_1} {β : Type u_2} (G : Graph α β) (w : WList α β) : Prop

G.IsPath P means that w is a walk of G with no repeated vertices (and therefore no repeated edges).

• isWalk : G.IsWalk w
• nodup : w.vertex.Nodup

theorem Graph.isPath_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (w : WList α β) : G.IsPath w ↔ G.IsWalk w ∧ w.vertex.Nodup

theorem Graph.nil_isPath {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} (hx : x ∈ G.vertexSet) : G.IsPath (WList.nil x)

@[simp]

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

@[simp]

theorem Graph.IsPath.first_eq_last_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (h : G.IsPath P) : P.first = P.last ↔ P.Nil

@[simp]

theorem Graph.cons_isPath_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {P : WList α β} : G.IsPath (WList.cons x e P) ↔ G.IsLink e x P.first ∧ G.IsPath P ∧ x ∉ P

theorem Graph.IsPath.cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (he : G.IsLink e x P.first) (hxP : x ∉ P) : G.IsPath (WList.cons x e P)

@[simp]

theorem Graph.IsPath.of_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {P : WList α β} (h : G.IsPath (WList.cons x e P)) : G.IsPath P

theorem Graph.IsPath.isTrail {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (h : G.IsPath P) : G.IsTrail P

theorem Graph.IsPath.reverse {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hp : G.IsPath P) : G.IsPath P.reverse

@[simp]

theorem Graph.reverse_isPath_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} : G.IsPath P.reverse ↔ G.IsPath P

@[simp]

theorem Graph.concat_isPath_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {P : WList α β} : G.IsPath (P.concat e x) ↔ G.IsPath P ∧ G.IsLink e P.last x ∧ x ∉ P

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

theorem Graph.IsPath.noloop {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} [DecidableEq α] (h : G.IsPath P) : P.NoLoop

theorem Graph.IsLink.walk_isPath {α : Type u_1} {β : Type u_2} {u v : α} {e : β} {G : Graph α β} (h : G.IsLink e u v) (hne : u ≠ v) : G.IsPath h.walk

theorem Graph.IsPath.edge_nodup {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (h : G.IsPath P) : P.edge.Nodup

theorem Graph.IsPath.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {P : WList α β} (hP : G.IsPath P) (hle : G ≤ H) : H.IsPath P

theorem Graph.IsPath.vertexSet_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : P.vertexSet ⊆ G.vertexSet

theorem Graph.IsPath.edgeSet_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : P.edgeSet ⊆ G.edgeSet

theorem Graph.IsPath.induce {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {X : Set α} (hP : G.IsPath P) (hX : P.vertexSet ⊆ X) : G[X].IsPath P

theorem Graph.IsPath.deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {X : Set α} (hP : G.IsPath P) (hX : Disjoint P.vertexSet X) : (G.deleteVerts X).IsPath P

theorem Graph.IsPath.deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) {F : Set β} (hF : Disjoint P.edgeSet F) : (G.deleteEdges F).IsPath P

theorem Graph.IsPath.sublist {α : Type u_1} {β : Type u_2} {G : Graph α β} {P P₀ : WList α β} (hP : G.IsPath P) (hP₀ : P₀.IsSublist P) : G.IsPath P₀

theorem Graph.IsPath.prefix {α : Type u_1} {β : Type u_2} {G : Graph α β} {P P₀ : WList α β} (hP : G.IsPath P) (hP₀ : P₀.IsPrefix P) : G.IsPath P₀

theorem Graph.IsPath.suffix {α : Type u_1} {β : Type u_2} {G : Graph α β} {P P₀ : WList α β} (hP : G.IsPath P) (hP₀ : P₀.IsSuffix P) : G.IsPath P₀

theorem Graph.IsPath.infix {α : Type u_1} {β : Type u_2} {G : Graph α β} {P P₀ : WList α β} (hP : G.IsPath P) (hP₀ : P₀.IsInfix P) : G.IsPath P₀

theorem Graph.IsPath.infix_of_sublist {α : Type u_1} {β : Type u_2} {G : Graph α β} {P P₀ : WList α β} (hP : G.IsPath P) (hP₀ : P₀ ≤ P) : P₀.IsInfix P

theorem Graph.IsPath.eq_of_sublist_of_first_eq_last_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {P P₀ : WList α β} (hP : G.IsPath P) (hP₀ : P₀ ≤ P) (hf : P₀.first = P.first) (hl : P₀.last = P.last) : P₀ = P

theorem Graph.isPath_induce_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {X : Set α} (hXV : X ⊆ G.vertexSet) : G[X].IsPath P ↔ G.IsPath P ∧ P.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.isPath_induce_iff' {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {X : Set α} (hP : P.Nonempty) : G[X].IsPath P ↔ G.IsPath P ∧ P.vertexSet ⊆ X

@[simp]

theorem Graph.isPath_deleteVerts_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {X : Set α} : (G.deleteVerts X).IsPath P ↔ G.IsPath P ∧ Disjoint P.vertexSet X

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

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

@[simp]

theorem Graph.isPath_restrict_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {F : Set β} : (G.restrict F).IsPath P ↔ G.IsPath P ∧ P.edgeSet ⊆ F

@[simp]

theorem Graph.isPath_deleteEdges_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {F : Set β} : (G.deleteEdges F).IsPath P ↔ G.IsPath P ∧ Disjoint P.edgeSet F

theorem Graph.IsPath.append {α : Type u_1} {β : Type u_2} {G : Graph α β} {P Q : WList α β} (hP : G.IsPath P) (hQ : G.IsPath Q) (hPQ : P.last = Q.first) (h_inter : ∀ x ∈ P, x ∈ Q → x = P.last) : G.IsPath (P ++ Q)

theorem Graph.IsPath.of_append_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {P Q : WList α β} (hP : G.IsPath (P ++ Q)) (hPQ : P.last = Q.first) : G.IsPath P

theorem Graph.IsPath.of_append_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {P Q : WList α β} (hP : G.IsPath (P ++ Q)) : G.IsPath Q

theorem Graph.IsPath.eq_append_cons_of_edge_mem {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (heP : e ∈ P.edge) : ∃ (P₁ : WList α β) (P₂ : WList α β), G.IsPath P₁ ∧ G.IsPath P₂ ∧ e ∉ P₁.edge ∧ e ∉ P₂.edge ∧ P₁.vertex.Disjoint P₂.vertex ∧ P₁.edge.Disjoint P₂.edge ∧ P = P₁ ++ WList.cons P₁.last e P₂

theorem Graph.IsPath.eq_firstEdge_of_isLink_first {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (heP : e ∈ P.edge) (he : G.Inc e P.first) : e = WList.Nonempty.firstEdge P ⋯

An edge of a path P incident to the first vertex is the first edge.

theorem Graph.IsPath.first_eq_of_isLink_mem {α : Type u_1} {β : Type u_2} {x y : α} {e f : β} {G : Graph α β} {w : WList α β} (hP : G.IsPath (WList.cons x f w)) (heP : e ∈ (WList.cons x f w).edge) (hl : G.IsLink e x y) : e = f ∧ w.first = y

theorem Graph.IsPath.vertexSet_nontrivial_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : P.vertexSet.Nontrivial ↔ P.Nonempty

theorem Graph.IsPath.encard_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : P.vertexSet.encard = ↑P.length + 1

theorem Graph.IsPath.ncard_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : P.vertexSet.ncard = P.length + 1

theorem Graph.IsPath.vertex_length_eq_ncard {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : P.vertex.length = P.vertexSet.ncard

theorem Graph.IsPath.vertex_length_eq_encard {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : ↑P.vertex.length = P.vertexSet.encard

theorem Graph.IsPath.vertex_length_le_encard {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : ↑P.vertex.length ≤ G.vertexSet.encard

theorem Graph.IsPath.length_le_encard {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : ↑P.length + 1 ≤ G.vertexSet.encard

Every path has at most V(G).encard - 1 edges.

theorem Graph.IsPath.diff_Last_disjoint_of_append {α : Type u_1} {β : Type u_2} {G : Graph α β} {P₀ P₁ : WList α β} (hP : G.IsPath (P₀ ++ P₁)) : Disjoint (P₀.vertexSet \ {P₀.last}) P₁.vertexSet

theorem Graph.IsPath.disjoint_of_append_append {α : Type u_1} {β : Type u_2} {G : Graph α β} {P₀ P₁ P₂ : WList α β} (hP : G.IsPath (P₀ ++ P₁ ++ P₂)) (heq : P₀.last = P₁.first) (hP₁ : P₁.Nonempty) : Disjoint P₀.vertexSet P₂.vertexSet

theorem Graph.IsPath.inter_eq_singleton_of_append {α : Type u_1} {β : Type u_2} {G : Graph α β} {P₀ P₁ : WList α β} (hP : G.IsPath (P₀ ++ P₁)) (heq : P₀.last = P₁.first) : P₀.vertexSet ∩ P₁.vertexSet = {P₀.last}

theorem Graph.IsPath.not_nontrivial_of_dInc {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {e : β} {x y s t : α} (hP : G.IsPath P) (hfirst : P.first = s) (hlast : P.last = t) (he : P.DInc e x y) (hx : x = s ∨ x = t) (hy : y = s ∨ y = t) : ¬P.Nontrivial

theorem Graph.IsPath.not_nontrivial_of_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {e : β} {x y s t : α} (hP : G.IsPath P) (hfirst : P.first = s) (hlast : P.last = t) (he : P.IsLink e x y) (hx : x = s ∨ x = t) (hy : y = s ∨ y = t) : ¬P.Nontrivial

@[simp]

theorem Graph.IsPath.suffixFromVertex_of_dInc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {P : WList α β} [DecidableEq α] (hP : G.IsPath P) (h : P.DInc e x y) : P.suffixFromVertex x = WList.cons x e (P.suffixFromVertex y)

@[simp]

theorem Graph.IsPath.prefixUntilVertex_dInc_suffixFromVertex {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {P : WList α β} [DecidableEq α] (hP : G.IsPath P) (h : P.DInc e x y) : P.prefixUntilVertex x ++ WList.cons x e (P.suffixFromVertex y) = P

@[simp]

theorem Graph.IsPath.first_mem_suffixFromVertex_iff {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {P : WList α β} [DecidableEq α] (hP : G.IsPath P) (hx : x ∈ P) : P.first ∈ P.suffixFromVertex x ↔ P.first = x

theorem Graph.IsPath.eq_of_mem_prefixUntilVertex_suffixFromVertex {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} {P : WList α β} [DecidableEq α] (hP : G.IsPath P) (hypre : y ∈ P.prefixUntilVertex x) (hysuf : y ∈ P.suffixFromVertex x) (hx : x ∈ P) : x = y

Fixed ends. (To be cleaned up)

structure Graph.IsTrailFrom {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) (W : WList α β) extends G.IsTrail W, G.IsWalkFrom S T W : Prop

• isWalk : G.IsWalk W
• edge_nodup : W.edge.Nodup
• first_mem : W.first ∈ S
• last_mem : W.last ∈ T

theorem Graph.isTrailFrom_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) (W : WList α β) : G.IsTrailFrom S T W ↔ G.IsTrail W ∧ W.first ∈ S ∧ W.last ∈ T

structure Graph.IsPathFrom {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) (P : WList α β) extends G.IsPath P, G.IsWalkFrom S T P : Prop

• isWalk : G.IsWalk P
• nodup : P.vertex.Nodup
• first_mem : P.first ∈ S
• last_mem : P.last ∈ T
• eq_first_of_mem ⦃x : α⦄ : x ∈ P → x ∈ S → x = P.first
• eq_last_of_mem ⦃y : α⦄ : y ∈ P → y ∈ T → y = P.last

theorem Graph.isPathFrom_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) (P : WList α β) : G.IsPathFrom S T P ↔ G.IsPath P ∧ P.first ∈ S ∧ P.last ∈ T ∧ (∀ ⦃x : α⦄, x ∈ P → x ∈ S → x = P.first) ∧ ∀ ⦃y : α⦄, y ∈ P → y ∈ T → y = P.last

theorem Graph.IsPathFrom.isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T : Set α} (h : G.IsPathFrom S T P) : G.IsPath P

@[simp]

theorem Graph.nil_isPathFrom {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {S T : Set α} : G.IsPathFrom S T (WList.nil x) ↔ x ∈ G.vertexSet ∧ x ∈ S ∧ x ∈ T

theorem Graph.IsPathFrom.eq_first_iff_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T : Set α} (h : G.IsPathFrom S T P) (v : α) : v = P.first ↔ v ∈ P.vertexSet ∧ v ∈ S

@[simp]

theorem Graph.IsPathFrom.vertexSet_inter_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T : Set α} (h : G.IsPathFrom S T P) : P.vertexSet ∩ S = {P.first}

theorem Graph.IsPathFrom.eq_last_iff_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T : Set α} (h : G.IsPathFrom S T P) (v : α) : v = P.last ↔ v ∈ P.vertexSet ∧ v ∈ T

@[simp]

theorem Graph.IsPathFrom.vertexSet_inter_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T : Set α} (h : G.IsPathFrom S T P) : P.vertexSet ∩ T = {P.last}

@[simp]

theorem Graph.IsPathFrom.last_mem_iff_nil {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T : Set α} (h : G.IsPathFrom S T P) : P.last ∈ S ↔ P.Nil

@[simp]

theorem Graph.IsPathFrom.first_mem_iff_nil {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T : Set α} (h : G.IsPathFrom S T P) : P.first ∈ T ↔ P.Nil

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

theorem Graph.IsPathFrom.subset_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T S₀ : Set α} (hP : G.IsPathFrom S T P) (hS₀ : S₀ ⊆ S) (hx : P.first ∈ S₀) : G.IsPathFrom S₀ T P

theorem Graph.IsPathFrom.subset_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T T₀ : Set α} (hP : G.IsPathFrom S T P) (hT₀ : T₀ ⊆ T) (hx : P.last ∈ T₀) : G.IsPathFrom S T₀ P

theorem Graph.IsPathFrom.subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T S₀ T₀ : Set α} (hP : G.IsPathFrom S T P) (hS₀ : S₀ ⊆ S) (hT₀ : T₀ ⊆ T) (hx : P.first ∈ S₀) (hy : P.last ∈ T₀) : G.IsPathFrom S₀ T₀ P

theorem Graph.isPathFrom_vertexSet_inter_left_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T : Set α} : G.IsPathFrom (G.vertexSet ∩ S) T P ↔ G.IsPathFrom S T P

theorem Graph.isPathFrom_vertexSet_inter_right_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T : Set α} : G.IsPathFrom S (G.vertexSet ∩ T) P ↔ G.IsPathFrom S T P

theorem Graph.IsPathFrom.diff_left_of_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T X : Set α} (hP : G.IsPathFrom S T P) (hdj : Disjoint P.vertexSet X) : G.IsPathFrom (S \ X) T P

theorem Graph.IsPathFrom.diff_right_of_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T X : Set α} (hP : G.IsPathFrom S T P) (hdj : Disjoint P.vertexSet X) : G.IsPathFrom S (T \ X) P

theorem Graph.IsPathFrom.left_of_symmdiff_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T S₀ : Set α} (hP : G.IsPathFrom S T P) (hA : Disjoint P.vertexSet (symmDiff S S₀)) : G.IsPathFrom S₀ T P

theorem Graph.IsPathFrom.right_of_symmdiff_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T T₀ : Set α} (hP : G.IsPathFrom S T P) (hA : Disjoint P.vertexSet (symmDiff T T₀)) : G.IsPathFrom S T₀ P

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

theorem Graph.IsPathFrom.isPathFrom_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {P : WList α β} {S T : Set α} (h : G.IsPathFrom S T P) (hle : H ≤ G) (hss : P.edgeSet ⊆ H.edgeSet) (hne : P.first ∈ H.vertexSet) : H.IsPathFrom S T P

theorem Graph.IsPathFrom.of_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T X : Set α} (hP : (G.deleteVerts X).IsPathFrom S T P) : G.IsPathFrom (S ∪ X) (T ∪ X) P

theorem Graph.IsPathFrom.of_deleteVerts' {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T X : Set α} (hP : (G.deleteVerts X).IsPathFrom S T P) : G.IsPathFrom S T P

theorem Graph.IsPathFrom.deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T X : Set α} (hP : G.IsPathFrom S T P) (hdj : Disjoint P.vertexSet X) : (G.deleteVerts X).IsPathFrom S T P

theorem Graph.isPathFrom_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {P : WList α β} {S T : Set α} : G.IsPathFrom S T (WList.cons x e P) ↔ x ∈ S ∧ x ∉ T ∧ G.IsLink e x P.first ∧ Disjoint S P.vertexSet ∧ G.IsPathFrom {P.first} T P

theorem Graph.IsPathFrom.append_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {P₀ P₁ : WList α β} {S T : Set α} (hP₀ : G.IsPathFrom S T P₀) (hP₁ : G.IsPath P₁) (h₁T : P₁.vertexSet ⊆ T) (h₁₂ : P₀.last = P₁.first) : G.IsPathFrom (S \ (P₁.vertexSet \ {P₁.first})) (T \ (P₁.vertexSet \ {P₁.last})) (P₀ ++ P₁)

theorem Graph.IsPathFrom.append_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {P₀ P₁ : WList α β} {S T : Set α} (hP₁ : G.IsPathFrom S T P₁) (hP₀ : G.IsPath P₀) (h₀S : P₀.vertexSet ⊆ S) (h₀₁ : P₀.last = P₁.first) : G.IsPathFrom (S \ (P₀.vertexSet \ {P₀.first})) (T \ (P₀.vertexSet \ {P₀.last})) (P₀ ++ P₁)

theorem Graph.IsPathFrom.prefixUntil {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T T' : Set α} (hP : G.IsPathFrom S T P) (h : ∃ x ∈ P, x ∈ T') [DecidablePred fun (x : α) => x ∈ T'] : G.IsPathFrom S T' (P.prefixUntil fun (x : α) => x ∈ T')

theorem Graph.IsPathFrom.suffixFromLast {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S S' T : Set α} (hP : G.IsPathFrom S T P) (h : ∃ x ∈ P, x ∈ S') [DecidablePred fun (x : α) => x ∈ S'] : G.IsPathFrom S' T (P.suffixFromLast fun (x : α) => x ∈ S')

theorem Graph.isPathFrom_cons_subgraph {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} {P : WList α β} {T : Set α} (hle : H ≤ G) : G.IsPathFrom H.vertexSet T (WList.cons x e P) ↔ x ∈ H.vertexSet ∧ x ∉ T ∧ G.IsLink e x P.first ∧ e ∉ H.edgeSet ∧ Disjoint H.vertexSet P.vertexSet ∧ G.IsPathFrom {P.first} T P

A version of isPathFrom_cons where the source set is a subgraph H, and we get the additional condition that the first edge is not an edge of H.

theorem Graph.IsPathFrom.notMem_left_of_dInc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {P : WList α β} {S T : Set α} (h : G.IsPathFrom S T P) (hP : P.DInc e x y) : y ∉ S

theorem Graph.IsPathFrom.notMem_right_of_dInc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {P : WList α β} {S T : Set α} (h : G.IsPathFrom S T P) (hP : P.DInc e x y) : x ∉ T

theorem Graph.IsPath.betweenSets_isPathFrom {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {S T : Set α} [DecidablePred fun (x : α) => x ∈ S] [DecidablePred fun (x : α) => x ∈ T] (hP : G.IsPath P) (hf : P.first ∈ S) (hl : P.last ∈ T) : G.IsPathFrom S T (P.betweenSets S T)

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

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

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

theorem Graph.IsWalk.isWalkFrom {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {S T : Set α} (hVd : G.IsWalk w) (hfirst : w.first ∈ S) (hlast : w.last ∈ T) : G.IsWalkFrom S T w

theorem Graph.IsWalk.isTrailFrom {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {S T : Set α} (hVd : G.IsWalk w) (hedge : w.edge.Nodup) (hfirst : w.first ∈ S) (hlast : w.last ∈ T) : G.IsTrailFrom S T w

theorem Graph.IsTrail.isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} (hT : G.IsTrail w) (hvertex : w.vertex.Nodup) : G.IsPath w

theorem Graph.IsTrail.isTrailFrom {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {S T : Set α} (hT : G.IsTrail w) (hfirst : w.first ∈ S) (hlast : w.last ∈ T) : G.IsTrailFrom S T w

theorem Graph.nil_isWalkFrom {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {S T : Set α} (hx : x ∈ G.vertexSet) (hxS : x ∈ S) (hxT : x ∈ T) : G.IsWalkFrom S T (WList.nil x)

@[simp]

theorem Graph.nil_isWalkFrom_iff {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {S T : Set α} : G.IsWalkFrom S T (WList.nil x) ↔ x ∈ G.vertexSet ∧ x ∈ S ∧ x ∈ T

@[simp]

theorem Graph.cons_isTrailFrom {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {w : WList α β} {S T : Set α} : G.IsTrailFrom S T (WList.cons x e w) ↔ G.IsTrail w ∧ G.IsLink e x w.first ∧ e ∉ w.edge ∧ x ∈ S ∧ w.last ∈ T

@[simp]

theorem Graph.nil_isTrailFrom {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {S T : Set α} : G.IsTrailFrom S T (WList.nil x) ↔ x ∈ G.vertexSet ∧ x ∈ S ∧ x ∈ T

The type of paths

@[reducible, inline]

abbrev Graph.Path {α : Type u_1} {β : Type u_2} (G : Graph α β) : Type (max u_1 u_2)

A path bundled with its proof of validity in G.

Equations

• G.Path = { P : WList α β // G.IsPath P }

def Graph.Path.first {α : Type u_1} {β : Type u_2} {G : Graph α β} (P : G.Path) : ↑G.vertexSet

The first vertex of a bundled path, intrinsically typed in the graph's vertex set.

Equations

• P.first = ⟨(↑P).first, ⋯⟩

def Graph.Path.last {α : Type u_1} {β : Type u_2} {G : Graph α β} (P : G.Path) : ↑G.vertexSet

The last vertex of a bundled path, intrinsically typed in the graph's vertex set.

Equations

• P.last = ⟨(↑P).last, ⋯⟩

def Graph.Path.reverse {α : Type u_1} {β : Type u_2} {G : Graph α β} (P : G.Path) : G.Path

Reverse a bundled path.

Equations

• P.reverse = ⟨(↑P).reverse, ⋯⟩

def Graph.Path.vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (P : G.Path) : Set ↑G.vertexSet

The vertices used by a bundled path, intrinsically typed in the graph's vertex set.

Equations

• P.vertexSet = {x : ↑G.vertexSet | ↑x ∈ ↑P}

def Graph.Path.edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (P : G.Path) : Set ↑G.edgeSet

The edges used by a bundled path, intrinsically typed in the graph's edge set.

Equations

• P.edgeSet = {e : ↑G.edgeSet | ↑e ∈ (↑P).edge}

Longest Paths

theorem Graph.mem_of_adj_first_of_maximal_isPath {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {P : WList α β} (hP : Maximal (fun (P : WList α β) => G.IsPath P) P) (hx : G.Adj x P.first) : x ∈ P